GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/util/indexed_root_predicate.h Lines: 0 6 0.0 % Date: 2021-03-23 Branches: 0 0 0.0 %

 Line Exec Source 1 /********************* */ 2 /*! \file indexed_root_predicate.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Gereon Kremer 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS 8 ** in the top-level source directory and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Utils for indexed root predicates. 13 ** 14 ** Some utils for indexed root predicates. 15 **/ 16 17 #include "cvc4_public.h" 18 19 #ifndef CVC4__UTIL__INDEXED_ROOT_PREDICATE_H 20 #define CVC4__UTIL__INDEXED_ROOT_PREDICATE_H 21 22 namespace CVC4 { 23 24 /** 25 * The structure representing the index of a root predicate. 26 * An indexed root predicate has the form 27 * IRP_k(x ~ 0, p) 28 * where k is a positive integer (d_index), x is a real variable, 29 * ~ an arithmetic relation symbol and p a (possibly multivariate polynomial). 30 * The evaluation of the predicate is obtained by comparing the k'th root of p 31 * (as polynomial in x) to the value of x according to the relation symbol ~. 32 * Note that p may be multivariate: in this case we can only evaluate with 33 * respect to a (partial) variable assignment, that (at least) contains values 34 * for all variables from p except x. 35 * 36 * Some examples: 37 * IRP_1(x > 0, x) <=> x > 0 38 * IRP_1(x < 0, x*x-1) <=> x < -1 39 * IRP_2(x < 0, x*x-1) <=> x < 1 40 * IRP_1(x = 0, x*x-2) <=> x = -sqrt(2) 41 * IRP_1(x = 0, x*x-y), y=3 <=> x = -sqrt(3) 42 */ 43 struct IndexedRootPredicate 44 { 45 /** The index of the root */ 46 std::uint64_t d_index; 47 48 IndexedRootPredicate(unsigned index) : d_index(index) {} 49 50 bool operator==(const IndexedRootPredicate& irp) const 51 { 52 return d_index == irp.d_index; 53 } 54 }; /* struct IndexedRootPredicate */ 55 56 inline std::ostream& operator<<(std::ostream& os, 57 const IndexedRootPredicate& irp); 58 inline std::ostream& operator<<(std::ostream& os, 59 const IndexedRootPredicate& irp) 60 { 61 return os << "k=" << irp.d_index; 62 } 63 64 struct IndexedRootPredicateHashFunction 65 { 66 std::size_t operator()(const IndexedRootPredicate& irp) const 67 { 68 return irp.d_index; 69 } 70 }; /* struct IndexedRootPredicateHashFunction */ 71 72 } // namespace CVC4 73 74 #endif

 Generated by: GCOVR (Version 3.2)