diff options
Diffstat (limited to 'src/theory')
118 files changed, 451 insertions, 427 deletions
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index ed7f54182..cd1014e38 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -25,9 +25,10 @@ #include <unordered_map> -#include "expr/node.h" -#include "context/cdo.h" #include "context/cdinsert_hashmap.h" +#include "context/cdo.h" +#include "expr/node.h" +#include "util/integer.h" namespace cvc5 { namespace preprocessing { diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index 724f83e07..3ca649211 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -16,6 +16,7 @@ #include "theory/arith/arith_msum.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index b8135127d..4d632e043 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -16,6 +16,8 @@ * \todo document this file */ +#include "theory/arith/arith_rewriter.h" + #include <set> #include <sstream> #include <stack> @@ -23,11 +25,12 @@ #include "smt/logic_exception.h" #include "theory/arith/arith_msum.h" -#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" #include "theory/arith/operator_elim.h" #include "theory/theory.h" +#include "util/bitvector.h" +#include "util/divisible.h" #include "util/iand.h" namespace cvc5 { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 8ada48cfe..4ab0b313b 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -36,6 +36,7 @@ namespace cvc5 { class ProofNodeManager; +class EagerProofGenerator; namespace context { class Context; @@ -43,8 +44,6 @@ class UserContext; } namespace theory { - -class EagerProofGenerator; struct EeSetupInfo; namespace eq { diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index fce071e6e..f6306049b 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -97,14 +97,13 @@ namespace cvc5 { class ProofNodeManager; +class EagerProofGenerator; namespace context { class Context; } namespace theory { -class EagerProofGenerator; - namespace arith { class Comparison; diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index e1eda5d85..396befb35 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -44,10 +44,11 @@ operator ARCCOTANGENT 1 "arc cotangent" operator SQRT 1 "square root" constant DIVISIBLE_OP \ - ::cvc5::Divisible \ - ::cvc5::DivisibleHashFunction \ - "util/divisible.h" \ - "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class" + struct \ + Divisible \ + ::cvc5::DivisibleHashFunction \ + "util/divisible.h" \ + "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class" sort REAL_TYPE \ Cardinality::REALS \ @@ -63,7 +64,8 @@ sort INTEGER_TYPE \ "integer type" constant CONST_RATIONAL \ - ::cvc5::Rational \ + class \ + Rational \ ::cvc5::RationalHashFunction \ "util/rational.h" \ "a multiple-precision rational constant; payload is an instance of the cvc5::Rational class" @@ -82,10 +84,11 @@ operator GEQ 2 "greater than or equal, x >= y" # represents an indexed root predicate. See util/indexed_root_predicate.h for more documentation. constant INDEXED_ROOT_PREDICATE_OP \ - ::cvc5::IndexedRootPredicate \ - ::cvc5::IndexedRootPredicateHashFunction \ - "util/indexed_root_predicate.h" \ - "operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class" + struct \ + IndexedRootPredicate \ + ::cvc5::IndexedRootPredicateHashFunction \ + "util/indexed_root_predicate.h" \ + "operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class" parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial" operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" @@ -157,10 +160,11 @@ typerule PI ::cvc5::theory::arith::RealNullaryOperatorTypeRule # (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2))) # for all integers i1, i2. constant IAND_OP \ - ::cvc5::IntAnd \ - "::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \ - "util/iand.h" \ - "operator for integer AND; payload is an instance of the cvc5::IntAnd class" + struct \ + IntAnd \ + "::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \ + "util/iand.h" \ + "operator for integer AND; payload is an instance of the cvc5::IntAnd class" parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms" typerule IAND_OP ::cvc5::theory::arith::IAndOpTypeRule diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index 374a7e4ef..a74913d99 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -19,6 +19,7 @@ #include "proof/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" +#include "util/indexed_root_predicate.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index c1937797e..7db6c266f 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -23,6 +23,7 @@ #include "theory/arith/nl/ext/monomial.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index d6b732eb9..4c79564e3 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -23,6 +23,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index bf38bc8f0..330cd57a3 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -22,6 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 9efa9c0f2..d2a5e628a 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -22,6 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index cb2fdab6f..8200ff08e 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -24,6 +24,7 @@ #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/bitvector.h" #include "util/iand.h" using namespace cvc5::kind; diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index cc35a4675..45881e1bb 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -20,6 +20,7 @@ #include "cvc5_private.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index e3094ae88..b25fa4f69 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -56,9 +56,11 @@ #include "util/statistics_stats.h" namespace cvc5 { -namespace theory { class EagerProofGenerator; + +namespace theory { + class TheoryModel; namespace arith { diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp index ba4c7dcb5..1ba501f90 100644 --- a/src/theory/arith/theory_arith_type_rules.cpp +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -15,6 +15,8 @@ #include "theory/arith/theory_arith_type_rules.h" +#include "util/rational.h" + namespace cvc5 { namespace theory { namespace arith { diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index e39f30c6e..67abc149d 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -36,7 +36,8 @@ operator EQ_RANGE 4 "equality of two arrays over an index range lower/upper" # storeall t e is \all i in indexType(t) <= e constant STORE_ALL \ - ::cvc5::ArrayStoreAll \ + class \ + ArrayStoreAll \ ::cvc5::ArrayStoreAllHashFunction \ "expr/array_store_all.h" \ "array store-all; payload is an instance of the cvc5::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 0bdccfd17..ea18b3180 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -18,6 +18,7 @@ #include <map> #include <memory> +#include "expr/array_store_all.h" #include "expr/kind.h" #include "expr/node_algorithm.h" #include "options/arrays_options.h" diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 8ad7a5f95..1072ffaf4 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -16,9 +16,12 @@ * \todo document this file */ -#include "expr/attribute.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "expr/array_store_all.h" +#include "expr/attribute.h" +#include "util/cardinality.h" + namespace cvc5 { namespace theory { namespace arrays { diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index 04a2f1a74..6d16e4020 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -16,8 +16,10 @@ #include "theory/arrays/theory_arrays_type_rules.h" // for array-constant attributes +#include "expr/array_store_all.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/type_enumerator.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 181a42da4..6fc026b19 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -18,10 +18,11 @@ #ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H #define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H -#include "theory/type_enumerator.h" -#include "expr/type_node.h" +#include "expr/array_store_all.h" #include "expr/kind.h" +#include "expr/type_node.h" #include "theory/rewriter.h" +#include "theory/type_enumerator.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 47eb90f45..203903d88 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -21,6 +21,7 @@ #include "theory/bags/solver_state.h" #include "theory/bags/term_registry.h" #include "theory/uf/equality_engine_iterator.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 3d1a94f22..b9f620d51 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -15,7 +15,9 @@ #include "theory/bags/bags_rewriter.h" +#include "expr/emptybag.h" #include "theory/bags/normal_form.h" +#include "util/rational.h" #include "util/statistics_registry.h" using namespace cvc5::kind; diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 6286f20b7..556dc76d6 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -21,6 +21,7 @@ #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" #include "theory/uf/equality_engine.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index 038e7dd7f..795410239 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -16,7 +16,8 @@ properties check presolve # constants constant EMPTYBAG \ - ::cvc5::EmptyBag \ + class \ + EmptyBag \ ::cvc5::EmptyBagHashFunction \ "expr/emptybag.h" \ "the empty bag constant; payload is an instance of the cvc5::EmptyBag class" @@ -50,7 +51,8 @@ operator BAG_COUNT 2 "multiplicity of an element in a bag" operator DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" constant MK_BAG_OP \ - ::cvc5::MakeBagOp \ + class \ + MakeBagOp \ ::cvc5::MakeBagOpHashFunction \ "theory/bags/make_bag_op.h" \ "operator for MK_BAG; payload is an instance of the cvc5::MakeBagOp class" diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp index 08142e6f9..ec32d0138 100644 --- a/src/theory/bags/normal_form.cpp +++ b/src/theory/bags/normal_form.cpp @@ -14,8 +14,10 @@ */ #include "normal_form.h" +#include "expr/emptybag.h" #include "theory/sets/normal_form.h" #include "theory/type_enumerator.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index 2db38e62b..659886e83 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -15,6 +15,7 @@ #include "theory/bags/term_registry.h" +#include "expr/emptyset.h" #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 4695c1db7..be9e0cd4d 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -18,6 +18,7 @@ #include "expr/emptybag.h" #include "theory/rewriter.h" #include "theory_bags_type_enumerator.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 133059cd0..d820ce6e1 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -18,7 +18,11 @@ #include <sstream> #include "base/check.h" +#include "expr/emptybag.h" +#include "theory/bags/make_bag_op.h" #include "theory/bags/normal_form.h" +#include "util/cardinality.h" +#include "util/rational.h" namespace cvc5 { namespace theory { @@ -279,6 +283,11 @@ TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager, return setType; } +Cardinality BagsProperties::computeCardinality(TypeNode type) +{ + return Cardinality::INTEGERS; +} + bool BagsProperties::isWellFounded(TypeNode type) { return type[0].isWellFounded(); diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index a633d604f..487423309 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -125,10 +125,7 @@ struct ToSetTypeRule struct BagsProperties { - static Cardinality computeCardinality(TypeNode type) - { - return Cardinality::INTEGERS; - } + static Cardinality computeCardinality(TypeNode type); static bool isWellFounded(TypeNode type); diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 74e1a7cd8..d01ec081e 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -34,11 +34,9 @@ namespace cvc5 { class ProofGenerator; class ProofNode; - -namespace theory { - class EagerProofGenerator; +namespace theory { namespace booleans { /** diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 6560cdd1a..da5642057 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -19,6 +19,7 @@ sort BOOLEAN_TYPE \ "Boolean type" constant CONST_BOOLEAN \ + skip \ bool \ ::cvc5::BoolHashFunction \ "util/bool.h" \ diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index f7e788e9a..6c4e0f96b 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -19,6 +19,7 @@ #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 44d337c28..a5c63522d 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -16,11 +16,13 @@ * \todo document this file */ +#include "theory/booleans/theory_bool_rewriter.h" + #include <algorithm> #include <unordered_set> #include "expr/node_value.h" -#include "theory/booleans/theory_bool_rewriter.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index dffe0baf3..d4a8782b5 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -119,12 +119,14 @@ # For consistency these should start with "APPLY_", but this is # not enforced. # -# constant K T Hasher header ["comment"] +# constant K F T Hasher header ["comment"] # -# Declares a constant kind K. T is the C++ type representing the -# constant internally (and it should be -# ::fully::qualified::like::this), and header is the header needed -# to define it. Hasher is a hash functor type defined like this: +# Declares a constant kind K. F is the type of the forward declaration to +# generate (e.g., `class`, `struct`). If F is `skip` then then no forward +# declaration is generated. T is the C++ type representing the constant +# internally (the type is expected to be in the cvc5 namespace), and header +# is the header needed to define it. Hasher is a hash functor type defined +# like this: # # struct MyHashFcn { # size_t operator()(const T& val) const; @@ -263,7 +265,8 @@ well-founded SORT_TYPE \ "::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" constant UNINTERPRETED_CONSTANT \ - ::cvc5::UninterpretedConstant \ + class \ + UninterpretedConstant \ ::cvc5::UninterpretedConstantHashFunction \ "expr/uninterpreted_constant.h" \ "the kind of expressions representing uninterpreted constants; payload is an instance of the cvc5::UninterpretedConstant class (used in models)" @@ -273,7 +276,8 @@ enumerator SORT_TYPE \ "theory/builtin/type_enumerator.h" constant ABSTRACT_VALUE \ - ::cvc5::AbstractValue \ + class \ + AbstractValue \ ::cvc5::AbstractValueHashFunction \ "util/abstract_value.h" \ "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the cvc5::AbstractValue class (used in models)" @@ -284,7 +288,8 @@ typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. constant BUILTIN \ - ::cvc5::Kind \ + skip \ + Kind \ ::cvc5::kind::KindHashFunction \ "expr/kind.h" \ "the kind of expressions representing built-in operators" @@ -301,7 +306,8 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body" constant TYPE_CONSTANT \ - ::cvc5::TypeConstant \ + skip \ + TypeConstant \ ::cvc5::TypeConstantHashFunction \ "expr/kind.h" \ "a representation for basic types" diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 9dfc9418f..7ec0525c9 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -26,39 +26,6 @@ using namespace cvc5::kind; namespace cvc5 { namespace theory { - -const char* toString(MethodId id) -{ - switch (id) - { - case MethodId::RW_REWRITE: return "RW_REWRITE"; - case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE"; - case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT"; - case MethodId::RW_EVALUATE: return "RW_EVALUATE"; - case MethodId::RW_IDENTITY: return "RW_IDENTITY"; - case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE"; - case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST"; - case MethodId::SB_DEFAULT: return "SB_DEFAULT"; - case MethodId::SB_LITERAL: return "SB_LITERAL"; - case MethodId::SB_FORMULA: return "SB_FORMULA"; - case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL"; - case MethodId::SBA_SIMUL: return "SBA_SIMUL"; - case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT"; - default: return "MethodId::Unknown"; - }; -} - -std::ostream& operator<<(std::ostream& out, MethodId id) -{ - out << toString(id); - return out; -} - -Node mkMethodId(MethodId id) -{ - return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id))); -} - namespace builtin { void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) @@ -250,17 +217,6 @@ Node BuiltinProofRuleChecker::applySubstitution(Node n, return ns; } -bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i) -{ - uint32_t index; - if (!getUInt32(n, index)) - { - return false; - } - i = static_cast<MethodId>(index); - return true; -} - Node BuiltinProofRuleChecker::checkInternal(PfRule id, const std::vector<Node>& children, const std::vector<Node>& args) @@ -455,58 +411,6 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, return Node::null(); } -bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args, - MethodId& ids, - MethodId& ida, - MethodId& idr, - size_t index) -{ - ids = MethodId::SB_DEFAULT; - ida = MethodId::SBA_SEQUENTIAL; - idr = MethodId::RW_REWRITE; - for (size_t offset = 0; offset <= 2; offset++) - { - if (args.size() > index + offset) - { - MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr); - if (!getMethodId(args[index + offset], id)) - { - Trace("builtin-pfcheck") - << "Failed to get id from " << args[index + offset] << std::endl; - return false; - } - } - else - { - break; - } - } - Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / " - << ida << " / " << idr << "\n"; - return true; -} - -void BuiltinProofRuleChecker::addMethodIds(std::vector<Node>& args, - MethodId ids, - MethodId ida, - MethodId idr) -{ - bool ndefRewriter = (idr != MethodId::RW_REWRITE); - bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL); - if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply) - { - args.push_back(mkMethodId(ids)); - } - if (ndefApply || ndefRewriter) - { - args.push_back(mkMethodId(ida)); - } - if (ndefRewriter) - { - args.push_back(mkMethodId(idr)); - } -} - bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid) { uint32_t i; diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 892fc7a4b..1e671a7b3 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Equality proof checker utility. + * Builtin proof checker utility. */ #include "cvc5_private.h" @@ -19,74 +19,13 @@ #define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H #include "expr/node.h" +#include "proof/method_id.h" #include "proof/proof_checker.h" #include "proof/proof_node.h" #include "theory/quantifiers/extended_rewrite.h" namespace cvc5 { namespace theory { - -/** - * Identifiers for rewriters and substitutions, which we abstractly - * classify as "methods". Methods have a unique identifier in the internal - * proof calculus implemented by the checker below. - * - * A "rewriter" is abstractly a method from Node to Node, where the output - * is semantically equivalent to the input. The identifiers below list - * various methods that have this contract. This identifier is used - * in a number of the builtin rules. - * - * A substitution is a method for turning a formula into a substitution. - */ -enum class MethodId : uint32_t -{ - //---------------------------- Rewriters - // Rewriter::rewrite(n) - RW_REWRITE, - // d_ext_rew.extendedRewrite(n); - RW_EXT_REWRITE, - // Rewriter::rewriteExtEquality(n) - RW_REWRITE_EQ_EXT, - // Evaluator::evaluate(n) - RW_EVALUATE, - // identity - RW_IDENTITY, - // theory preRewrite, note this is only intended to be used as an argument - // to THEORY_REWRITE in the final proof. It is not implemented in - // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE. - RW_REWRITE_THEORY_PRE, - // same as above, for theory postRewrite - RW_REWRITE_THEORY_POST, - //---------------------------- Substitutions - // (= x y) is interpreted as x -> y, using Node::substitute - SB_DEFAULT, - // P, (not P) are interpreted as P -> true, P -> false using Node::substitute - SB_LITERAL, - // P is interpreted as P -> true using Node::substitute - SB_FORMULA, - //---------------------------- Substitution applications - // multiple substitutions are applied sequentially - SBA_SEQUENTIAL, - // multiple substitutions are applied simultaneously - SBA_SIMUL, - // multiple substitutions are applied to fix point - SBA_FIXPOINT - // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to - // y gives: - // - f(g(x)) for SBA_SEQUENTIAL - // - f(z) for SBA_SIMUL - // - f(g(u)) for SBA_FIXPOINT - // Notice that SBA_FIXPOINT should provide a terminating rewrite system - // as a substitution, or else non-termination will occur during proof - // checking. -}; -/** Converts a rewriter id to a string. */ -const char* toString(MethodId id); -/** Write a rewriter id to out */ -std::ostream& operator<<(std::ostream& out, MethodId id); -/** Make a method id node */ -Node mkMethodId(MethodId id); - namespace builtin { /** A checker for builtin proofs */ @@ -166,26 +105,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker MethodId ids = MethodId::SB_DEFAULT, MethodId ida = MethodId::SBA_SEQUENTIAL, MethodId idr = MethodId::RW_REWRITE); - /** get a method identifier from a node, return false if we fail */ - static bool getMethodId(TNode n, MethodId& i); - /** - * Get method identifiers from args starting at the given index. Store their - * values into ids, ida, and idr. This method returns false if args does not - * contain valid method identifiers at position index in args. - */ - bool getMethodIds(const std::vector<Node>& args, - MethodId& ids, - MethodId& ida, - MethodId& idr, - size_t index); - /** - * Add method identifiers ids, ida and idr as nodes to args. This does not add - * ids, ida or idr if their values are the default ones. - */ - static void addMethodIds(std::vector<Node>& args, - MethodId ids, - MethodId ida, - MethodId idr); /** get a TheoryId from a node, return false if we fail */ static bool getTheoryId(TNode n, TheoryId& tid); diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 68d6e1ad1..0ee72fc5f 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -18,6 +18,7 @@ #include "theory/builtin/theory_builtin_rewriter.h" +#include "expr/array_store_all.h" #include "expr/attribute.h" #include "expr/node_algorithm.h" #include "theory/rewriter.h" diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index a448b2b69..f3c595720 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -17,11 +17,20 @@ #include "expr/attribute.h" #include "expr/skolem_manager.h" +#include "expr/uninterpreted_constant.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { namespace builtin { +TypeNode UninterpretedConstantTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return n.getConst<UninterpretedConstant>().getType(); +} + /** * Attribute for caching the ground term for each type. Maps TypeNode to the * skolem to return for mkGroundTerm. @@ -46,6 +55,25 @@ Node SortProperties::mkGroundTerm(TypeNode type) return k; } +Cardinality FunctionProperties::computeCardinality(TypeNode type) +{ + // Don't assert this; allow other theories to use this cardinality + // computation. + // + // Assert(type.getKind() == kind::FUNCTION_TYPE); + + Cardinality argsCard(1); + // get the largest cardinality of function arguments/return type + for (size_t i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) + { + argsCard *= type[i].getCardinality(); + } + + Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); + + return valueCard ^ argsCard; +} + } // namespace builtin } // namespace theory } // namespace cvc5 diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 87ba12ed1..00649a5af 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -93,9 +93,7 @@ class SExprTypeRule { class UninterpretedConstantTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - return n.getConst<UninterpretedConstant>().getType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); };/* class UninterpretedConstantTypeRule */ class AbstractValueTypeRule { @@ -202,22 +200,8 @@ class SortProperties { class FunctionProperties { public: - inline static Cardinality computeCardinality(TypeNode type) { - // Don't assert this; allow other theories to use this cardinality - // computation. - // - // Assert(type.getKind() == kind::FUNCTION_TYPE); - - Cardinality argsCard(1); - // get the largest cardinality of function arguments/return type - for(unsigned i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) { - argsCard *= type[i].getCardinality(); - } + static Cardinality computeCardinality(TypeNode type); - Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); - - return valueCard ^ argsCard; - } /** Function type is well-founded if its component sorts are */ static bool isWellFounded(TypeNode type) { diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index e6080ed4f..37758ad4a 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -24,6 +24,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" using namespace cvc5; using namespace cvc5::theory; diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index f5259dc93..f71f82ce1 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -25,6 +25,7 @@ #include "theory/bv/bitblast/bitblast_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 32b6dbd7a..ba545e48b 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -27,6 +27,7 @@ #include "context/cdo.h" #include "context/cdqueue.h" #include "context/context.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 3a9e460fe..65c1ec79c 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -29,6 +29,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "util/bitvector.h" using namespace cvc5::context; using namespace cvc5::prop; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 7c97d1bbc..2589418cc 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -23,6 +23,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/ext_theory.h" #include "theory/theory_model.h" +#include "util/rational.h" using namespace std; using namespace cvc5; diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 6af586735..9590d5522 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -13,19 +13,21 @@ properties check propagate presolve ppStaticLearn rewriter ::cvc5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" constant BITVECTOR_TYPE \ - ::cvc5::BitVectorSize \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \ - "util/bitvector.h" \ - "bit-vector type" + struct \ + BitVectorSize \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \ + "util/bitvector.h" \ + "bit-vector type" cardinality BITVECTOR_TYPE \ "::cvc5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \ "theory/bv/theory_bv_type_rules.h" constant CONST_BITVECTOR \ - ::cvc5::BitVector \ - ::cvc5::BitVectorHashFunction \ - "util/bitvector.h" \ - "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class" + class \ + BitVector \ + ::cvc5::BitVectorHashFunction \ + "util/bitvector.h" \ + "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class" enumerator BITVECTOR_TYPE \ "::cvc5::theory::bv::BitVectorEnumerator" \ @@ -101,59 +103,67 @@ operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bi ### parameterized operator kinds ---------------------------------------------- constant BITVECTOR_BITOF_OP \ - ::cvc5::BitVectorBitOf \ - ::cvc5::BitVectorBitOfHashFunction \ - "util/bitvector.h" \ - "operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class" + struct \ + BitVectorBitOf \ + ::cvc5::BitVectorBitOfHashFunction \ + "util/bitvector.h" \ + "operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class" parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term" constant BITVECTOR_EXTRACT_OP \ - ::cvc5::BitVectorExtract \ - ::cvc5::BitVectorExtractHashFunction \ - "util/bitvector.h" \ - "operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class" + struct \ + BitVectorExtract \ + ::cvc5::BitVectorExtractHashFunction \ + "util/bitvector.h" \ + "operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class" parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term" constant BITVECTOR_REPEAT_OP \ - ::cvc5::BitVectorRepeat \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \ - "util/bitvector.h" \ - "operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class" + struct \ + BitVectorRepeat \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \ + "util/bitvector.h" \ + "operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class" parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term" constant BITVECTOR_ROTATE_LEFT_OP \ - ::cvc5::BitVectorRotateLeft \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \ - "util/bitvector.h" \ - "operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class" + struct \ + BitVectorRotateLeft \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \ + "util/bitvector.h" \ + "operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class" parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term" constant BITVECTOR_ROTATE_RIGHT_OP \ - ::cvc5::BitVectorRotateRight \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \ - "util/bitvector.h" \ - "operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class" + struct \ + BitVectorRotateRight \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \ + "util/bitvector.h" \ + "operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term" constant BITVECTOR_SIGN_EXTEND_OP \ - ::cvc5::BitVectorSignExtend \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \ - "util/bitvector.h" \ - "operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class" + struct \ + BitVectorSignExtend \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \ + "util/bitvector.h" \ + "operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class" parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term" constant BITVECTOR_ZERO_EXTEND_OP \ - ::cvc5::BitVectorZeroExtend \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \ - "util/bitvector.h" \ - "operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class" + struct \ + BitVectorZeroExtend \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \ + "util/bitvector.h" \ + "operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class" parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term" constant INT_TO_BITVECTOR_OP \ - ::cvc5::IntToBitVector \ - "::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \ - "util/bitvector.h" \ - "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class" + struct \ + IntToBitVector \ + "::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \ + "util/bitvector.h" \ + "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class" parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term" ### type rules for non-parameterized operator kinds --------------------------- diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index af80ad00b..761f4efb2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -22,6 +22,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 45e313e48..5ead8a215 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -27,6 +27,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index e44d1c9b7..496a625ee 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -23,6 +23,7 @@ #include "options/bv_options.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 1e38aba0f..6d2ed4477 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -24,6 +24,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index d0579703d..476803c59 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -375,9 +375,13 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) { RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) { - Node resultNode = - LinearRewriteStrategy<RewriteRule<EvalComp>, RewriteRule<BvComp> >::apply( - node); + Node resultNode = LinearRewriteStrategy<RewriteRule<EvalComp>>::apply(node); + + if (node == resultNode && RewriteRule<BvComp>::applies(node)) + { + resultNode = RewriteRule<BvComp>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN, resultNode); + } return RewriteResponse(REWRITE_DONE, resultNode); } diff --git a/src/theory/bv/theory_bv_type_rules.cpp b/src/theory/bv/theory_bv_type_rules.cpp index 304a2b9cf..707b5f8bb 100644 --- a/src/theory/bv/theory_bv_type_rules.cpp +++ b/src/theory/bv/theory_bv_type_rules.cpp @@ -18,6 +18,8 @@ #include <algorithm> #include "expr/type_node.h" +#include "util/bitvector.h" +#include "util/cardinality.h" #include "util/integer.h" namespace cvc5 { diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 927a40b82..bc6096cbb 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -20,6 +20,8 @@ #include "expr/skolem_manager.h" #include "options/theory_options.h" #include "theory/theory.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index fca449917..712f5b822 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -23,6 +23,7 @@ #include <vector> #include "expr/node_manager.h" +#include "util/integer.h" namespace cvc5 { namespace theory { diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 063cefd49..6417b501e 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -28,10 +28,10 @@ namespace cvc5 { class TheoryEngine; class Env; +class EagerProofGenerator; namespace theory { -class EagerProofGenerator; class ModelManager; class SharedSolver; diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 744160c8b..e0e2f7ac8 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -15,14 +15,18 @@ #include "theory/datatypes/datatypes_rewriter.h" +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" +#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/tuple_project_op.h" +#include "util/rational.h" using namespace cvc5; using namespace cvc5::kind; diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 19f396a56..a4323a1d0 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -20,6 +20,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/model_manager.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 2642ae0c5..019efa950 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -23,10 +23,10 @@ #include "theory/inference_manager_buffered.h" namespace cvc5 { -namespace theory { class EagerProofGenerator; +namespace theory { namespace datatypes { /** diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 1b7808a8b..41d5ded76 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -48,10 +48,11 @@ parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is parameterized APPLY_UPDATER UPDATER_TYPE 2 "datatype updater application; first parameter is an update, second is a datatype term to update, third is the value to update with" constant DATATYPE_TYPE \ - ::cvc5::DatatypeIndexConstant \ - "::cvc5::DatatypeIndexConstantHashFunction" \ - "expr/datatype_index.h" \ - "a datatype type index" + class \ + DatatypeIndexConstant \ + "::cvc5::DatatypeIndexConstantHashFunction" \ + "expr/datatype_index.h" \ + "a datatype type index" cardinality DATATYPE_TYPE \ "%TYPE%.getDType().getCardinality(%TYPE%)" \ "expr/dtype.h" @@ -80,10 +81,11 @@ enumerator PARAMETRIC_DATATYPE \ parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \ "type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed" constant ASCRIPTION_TYPE \ - ::cvc5::AscriptionType \ - ::cvc5::AscriptionTypeHashFunction \ - "expr/ascription_type.h" \ - "a type parameter for type ascription; payload is an instance of the cvc5::AscriptionType class" + class \ + AscriptionType \ + ::cvc5::AscriptionTypeHashFunction \ + "expr/ascription_type.h" \ + "a type parameter for type ascription; payload is an instance of the cvc5::AscriptionType class" typerule APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRule typerule APPLY_SELECTOR ::cvc5::theory::datatypes::DatatypeSelectorTypeRule @@ -131,10 +133,11 @@ typerule MATCH_BIND_CASE ::cvc5::theory::datatypes::MatchBindCaseTypeRule constant TUPLE_PROJECT_OP \ - ::cvc5::TupleProjectOp \ - ::cvc5::TupleProjectOpHashFunction \ - "theory/datatypes/tuple_project_op.h" \ - "operator for TUPLE_PROJECT; payload is an instance of the cvc5::TupleProjectOp class" + class \ + TupleProjectOp \ + ::cvc5::TupleProjectOpHashFunction \ + "theory/datatypes/tuple_project_op.h" \ + "operator for TUPLE_PROJECT; payload is an instance of the cvc5::TupleProjectOp class" parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \ "projects a tuple from an existing tuple using indices passed in TupleProjectOp" diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index df644e9b2..6cb1f44e1 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -17,10 +17,13 @@ #include <sstream> +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/type_matcher.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/tuple_project_op.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index bf74347d0..582f11c72 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -15,6 +15,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 6cb2fdce9..39b48ece9 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -13,8 +13,10 @@ * Enumerators for datatypes. */ -#include "expr/dtype_cons.h" #include "theory/datatypes/type_enumerator.h" + +#include "expr/ascription_type.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 759c50db0..9ea121be4 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -21,6 +21,7 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" +#include "expr/uninterpreted_constant.h" #include "options/quantifiers_options.h" #include "theory/type_enumerator.h" diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 3a058772c..0d1b25549 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -800,17 +800,19 @@ Node FpConverter::rmToNode(const rm &r) const Node value = nm->mkNode( kind::ITE, nm->mkNode(kind::EQUAL, transVar, RNE), - nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RNA), - nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RTP), - nm->mkConst(ROUND_TOWARD_POSITIVE), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RTN), - nm->mkConst(ROUND_TOWARD_NEGATIVE), - nm->mkConst(ROUND_TOWARD_ZERO))))); + nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN), + nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RNA), + nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY), + nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RTP), + nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE), + nm->mkNode(kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RTN), + nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO))))); return value; } @@ -878,19 +880,19 @@ Node FpConverter::convert(TNode node) /******** Constants ********/ switch (current.getConst<RoundingMode>()) { - case ROUND_NEAREST_TIES_TO_EVEN: + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: d_rmMap.insert(current, traits::RNE()); break; - case ROUND_NEAREST_TIES_TO_AWAY: + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: d_rmMap.insert(current, traits::RNA()); break; - case ROUND_TOWARD_POSITIVE: + case RoundingMode::ROUND_TOWARD_POSITIVE: d_rmMap.insert(current, traits::RTP()); break; - case ROUND_TOWARD_NEGATIVE: + case RoundingMode::ROUND_TOWARD_NEGATIVE: d_rmMap.insert(current, traits::RTN()); break; - case ROUND_TOWARD_ZERO: + case RoundingMode::ROUND_TOWARD_ZERO: d_rmMap.insert(current, traits::RTZ()); break; default: Unreachable() << "Unknown rounding mode"; break; @@ -1100,7 +1102,7 @@ Node FpConverter::convert(TNode node) } break; - case kind::FLOATINGPOINT_PLUS: + case kind::FLOATINGPOINT_ADD: case kind::FLOATINGPOINT_SUB: case kind::FLOATINGPOINT_MULT: case kind::FLOATINGPOINT_DIV: @@ -1132,7 +1134,7 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { - case kind::FLOATINGPOINT_PLUS: + case kind::FLOATINGPOINT_ADD: d_fpMap.insert(current, symfpu::add<traits>(fpt(current.getType()), (*mode).second, diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp index dac0d5136..11bb05c70 100644 --- a/src/theory/fp/fp_expand_defs.cpp +++ b/src/theory/fp/fp_expand_defs.cpp @@ -16,6 +16,7 @@ #include "theory/fp/fp_expand_defs.h" #include "expr/skolem_manager.h" +#include "util/floatingpoint.h" namespace cvc5 { namespace theory { diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index d67738a63..fca5363fc 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -14,7 +14,8 @@ properties check # constants... constant CONST_FLOATINGPOINT \ - ::cvc5::FloatingPoint \ + class \ + FloatingPoint \ ::cvc5::FloatingPointHashFunction \ "util/floatingpoint.h" \ "a floating-point literal" @@ -22,9 +23,10 @@ typerule CONST_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointConstantTypeRul constant CONST_ROUNDINGMODE \ - ::cvc5::RoundingMode \ + "enum class" \ + RoundingMode \ ::cvc5::RoundingModeHashFunction \ - "util/floatingpoint.h" \ + "util/roundingmode.h" \ "a floating-point rounding mode" typerule CONST_ROUNDINGMODE ::cvc5::theory::fp::RoundingModeConstantTypeRule @@ -45,7 +47,8 @@ enumerator ROUNDINGMODE_TYPE \ constant FLOATINGPOINT_TYPE \ - ::cvc5::FloatingPointSize \ + class \ + FloatingPointSize \ ::cvc5::FloatingPointSizeHashFunction \ "util/floatingpoint.h" \ "floating-point type" @@ -80,8 +83,8 @@ typerule FLOATINGPOINT_ABS ::cvc5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_NEG 1 "floating-point negation" typerule FLOATINGPOINT_NEG ::cvc5::theory::fp::FloatingPointOperationTypeRule -operator FLOATINGPOINT_PLUS 3 "floating-point addition" -typerule FLOATINGPOINT_PLUS ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule +operator FLOATINGPOINT_ADD 3 "floating-point addition" +typerule FLOATINGPOINT_ADD ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_SUB 3 "floating-point sutraction" typerule FLOATINGPOINT_SUB ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule @@ -155,7 +158,8 @@ typerule FLOATINGPOINT_ISPOS ::cvc5::theory::fp::FloatingPointTestTypeRule constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPIEEEBitVector \ + class \ + FloatingPointToFPIEEEBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_fp from bit vector" @@ -167,7 +171,8 @@ typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::cvc5::theory::fp::FloatingPointT constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \ - ::cvc5::FloatingPointToFPFloatingPoint \ + class \ + FloatingPointToFPFloatingPoint \ "::cvc5::FloatingPointConvertSortHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_fp from floating point" @@ -180,7 +185,8 @@ typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointTo constant FLOATINGPOINT_TO_FP_REAL_OP \ - ::cvc5::FloatingPointToFPReal \ + class \ + FloatingPointToFPReal \ "::cvc5::FloatingPointConvertSortHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_fp from real" @@ -192,7 +198,8 @@ typerule FLOATINGPOINT_TO_FP_REAL ::cvc5::theory::fp::FloatingPointToFPRealTyp constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPSignedBitVector \ + class \ + FloatingPointToFPSignedBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_fp from signed bit vector" @@ -204,7 +211,8 @@ typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPoin constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPUnsignedBitVector \ + class \ + FloatingPointToFPUnsignedBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x10>" \ "util/floatingpoint.h" \ "operator for to_fp from unsigned bit vector" @@ -217,7 +225,8 @@ typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPo constant FLOATINGPOINT_TO_FP_GENERIC_OP \ - ::cvc5::FloatingPointToFPGeneric \ + class \ + FloatingPointToFPGeneric \ "::cvc5::FloatingPointConvertSortHashFunction<0x11>" \ "util/floatingpoint.h" \ "operator for a generic to_fp" @@ -232,7 +241,8 @@ typerule FLOATINGPOINT_TO_FP_GENERIC ::cvc5::theory::fp::FloatingPointToFPGene constant FLOATINGPOINT_TO_UBV_OP \ - ::cvc5::FloatingPointToUBV \ + class \ + FloatingPointToUBV \ "::cvc5::FloatingPointToBVHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_ubv" @@ -243,7 +253,8 @@ typerule FLOATINGPOINT_TO_UBV ::cvc5::theory::fp::FloatingPointToUBVTypeRule constant FLOATINGPOINT_TO_UBV_TOTAL_OP \ - ::cvc5::FloatingPointToUBVTotal \ + class \ + FloatingPointToUBVTotal \ "::cvc5::FloatingPointToBVHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_ubv_total" @@ -255,7 +266,8 @@ typerule FLOATINGPOINT_TO_UBV_TOTAL ::cvc5::theory::fp::FloatingPointToUBVTota constant FLOATINGPOINT_TO_SBV_OP \ - ::cvc5::FloatingPointToSBV \ + class \ + FloatingPointToSBV \ "::cvc5::FloatingPointToBVHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_sbv" @@ -266,7 +278,8 @@ typerule FLOATINGPOINT_TO_SBV ::cvc5::theory::fp::FloatingPointToSBVTypeRule constant FLOATINGPOINT_TO_SBV_TOTAL_OP \ - ::cvc5::FloatingPointToSBVTotal \ + class \ + FloatingPointToSBVTotal \ "::cvc5::FloatingPointToBVHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_sbv_total" diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index ecb8ba2b4..3d81a2995 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -29,6 +29,7 @@ #include "theory/output_channel.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "util/floatingpoint.h" using namespace std; @@ -100,7 +101,7 @@ void TheoryFp::finishInit() d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ABS); d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_NEG); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_PLUS); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ADD); // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SUB); // Removed d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MULT); d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_DIV); @@ -362,7 +363,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst<FloatingPointSize>())), - nm->mkConst(ROUND_TOWARD_POSITIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE), abstractValue)); Node bg = nm->mkNode( @@ -379,7 +380,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst<FloatingPointSize>())), - nm->mkConst(ROUND_TOWARD_NEGATIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE), abstractValue)); Node bl = nm->mkNode( diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 4f340e774..76f7d55cf 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -39,6 +39,7 @@ #include "base/check.h" #include "theory/bv/theory_bv_utils.h" #include "theory/fp/fp_converter.h" +#include "util/floatingpoint.h" namespace cvc5 { namespace theory { @@ -145,7 +146,8 @@ namespace rewrite { { Assert(node.getKind() == kind::FLOATINGPOINT_SUB); Node negation = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_NEG,node[2]); - Node addition = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_PLUS,node[0],node[1],negation); + Node addition = NodeManager::currentNM()->mkNode( + kind::FLOATINGPOINT_ADD, node[0], node[1], negation); return RewriteResponse(REWRITE_DONE, addition); } @@ -274,7 +276,7 @@ namespace rewrite { RewriteResponse reorderBinaryOperation (TNode node, bool isPreRewrite) { Kind k = node.getKind(); - Assert((k == kind::FLOATINGPOINT_PLUS) || (k == kind::FLOATINGPOINT_MULT)); + Assert((k == kind::FLOATINGPOINT_ADD) || (k == kind::FLOATINGPOINT_MULT)); Assert(!isPreRewrite); // Likely redundant in pre-rewrite if (node[1] > node[2]) { @@ -439,9 +441,9 @@ RewriteResponse neg(TNode node, bool isPreRewrite) node[0].getConst<FloatingPoint>().negate())); } -RewriteResponse plus(TNode node, bool isPreRewrite) +RewriteResponse add(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_PLUS); + Assert(node.getKind() == kind::FLOATINGPOINT_ADD); Assert(node.getNumChildren() == 3); RoundingMode rm(node[0].getConst<RoundingMode>()); @@ -450,8 +452,8 @@ RewriteResponse plus(TNode node, bool isPreRewrite) Assert(arg1.getSize() == arg2.getSize()); - return RewriteResponse( - REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2))); + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(arg1.add(rm, arg2))); } RewriteResponse mult(TNode node, bool isPreRewrite) @@ -1084,23 +1086,23 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RoundingMode arg0(node[0].getConst<RoundingMode>()); switch (arg0) { - case ROUND_NEAREST_TIES_TO_EVEN: + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: value = symfpuSymbolic::traits::RNE().getConst<BitVector>(); break; - case ROUND_NEAREST_TIES_TO_AWAY: + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: value = symfpuSymbolic::traits::RNA().getConst<BitVector>(); break; - case ROUND_TOWARD_POSITIVE: + case RoundingMode::ROUND_TOWARD_POSITIVE: value = symfpuSymbolic::traits::RTP().getConst<BitVector>(); break; - case ROUND_TOWARD_NEGATIVE: + case RoundingMode::ROUND_TOWARD_NEGATIVE: value = symfpuSymbolic::traits::RTN().getConst<BitVector>(); break; - case ROUND_TOWARD_ZERO: + case RoundingMode::ROUND_TOWARD_ZERO: value = symfpuSymbolic::traits::RTZ().getConst<BitVector>(); break; @@ -1142,7 +1144,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity; d_preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs; d_preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation; - d_preRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::identity; d_preRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::convertSubtractionToAddition; d_preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity; @@ -1233,8 +1235,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs; d_postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation; - d_postRewriteTable[kind::FLOATINGPOINT_PLUS] = - rewrite::reorderBinaryOperation; + d_postRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::reorderBinaryOperation; d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::reorderBinaryOperation; @@ -1325,7 +1326,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_constantFoldTable[kind::FLOATINGPOINT_FP] = constantFold::fpLiteral; d_constantFoldTable[kind::FLOATINGPOINT_ABS] = constantFold::abs; d_constantFoldTable[kind::FLOATINGPOINT_NEG] = constantFold::neg; - d_constantFoldTable[kind::FLOATINGPOINT_PLUS] = constantFold::plus; + d_constantFoldTable[kind::FLOATINGPOINT_ADD] = constantFold::add; d_constantFoldTable[kind::FLOATINGPOINT_MULT] = constantFold::mult; d_constantFoldTable[kind::FLOATINGPOINT_DIV] = constantFold::div; d_constantFoldTable[kind::FLOATINGPOINT_FMA] = constantFold::fma; @@ -1499,11 +1500,11 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) NodeManager* nm = NodeManager::currentNM(); - Node rne(nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN)); - Node rna(nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY)); - Node rtz(nm->mkConst(ROUND_TOWARD_POSITIVE)); - Node rtn(nm->mkConst(ROUND_TOWARD_NEGATIVE)); - Node rtp(nm->mkConst(ROUND_TOWARD_ZERO)); + Node rne(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN)); + Node rna(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY)); + Node rtz(nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE)); + Node rtn(nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE)); + Node rtp(nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO)); TNode rm(res.d_node[0]); diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index 5951decd4..b78ef24c7 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -17,6 +17,8 @@ // This is only needed for checking that components are only applied to leaves. #include "theory/theory.h" +#include "util/cardinality.h" +#include "util/floatingpoint.h" #include "util/roundingmode.h" namespace cvc5 { diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index c7c99adf2..edf297498 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -84,7 +84,7 @@ class RoundingModeEnumerator public: RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) : TypeEnumeratorBase<RoundingModeEnumerator>(type), - d_rm(ROUND_NEAREST_TIES_TO_EVEN), + d_rm(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN), d_enumerationComplete(false) { } @@ -99,11 +99,21 @@ class RoundingModeEnumerator RoundingModeEnumerator& operator++() override { switch (d_rm) { - case ROUND_NEAREST_TIES_TO_EVEN: d_rm = ROUND_TOWARD_POSITIVE; break; - case ROUND_TOWARD_POSITIVE: d_rm = ROUND_TOWARD_NEGATIVE; break; - case ROUND_TOWARD_NEGATIVE: d_rm = ROUND_TOWARD_ZERO; break; - case ROUND_TOWARD_ZERO: d_rm = ROUND_NEAREST_TIES_TO_AWAY; break; - case ROUND_NEAREST_TIES_TO_AWAY: d_enumerationComplete = true; break; + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: + d_rm = RoundingMode::ROUND_TOWARD_POSITIVE; + break; + case RoundingMode::ROUND_TOWARD_POSITIVE: + d_rm = RoundingMode::ROUND_TOWARD_NEGATIVE; + break; + case RoundingMode::ROUND_TOWARD_NEGATIVE: + d_rm = RoundingMode::ROUND_TOWARD_ZERO; + break; + case RoundingMode::ROUND_TOWARD_ZERO: + d_rm = RoundingMode::ROUND_NEAREST_TIES_TO_AWAY; + break; + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: + d_enumerationComplete = true; + break; default: Unreachable() << "Unknown rounding mode?"; break; } return *this; diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index fd204fffd..cfcc5f5a1 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/bv_inverter_utils.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" +#include "util/bitvector.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 0d85b8946..88da629a0 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1088,7 +1088,8 @@ bool CegInstantiator::doAddInstantiation(std::vector<Node>& vars, bool CegInstantiator::isEligibleForInstantiation(Node n) const { - if (n.getKind() != INST_CONSTANT && n.getKind() != SKOLEM) + Kind nk = n.getKind(); + if (nk != INST_CONSTANT && nk != SKOLEM && nk != BOOLEAN_TERM_VARIABLE) { return true; } diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index ca4abf497..fe47f1dd1 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -20,6 +20,7 @@ #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index d5af43242..83234d115 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 7ee22dc5b..7072b77e1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -18,6 +18,7 @@ #include <sstream> #include <stack> +#include "expr/ascription_type.h" #include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" @@ -30,6 +31,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/strings/word.h" +#include "util/floatingpoint.h" using namespace cvc5::kind; @@ -866,7 +868,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } // ternary ops with RM std::vector<Kind> ternary_rm_kinds = { - FLOATINGPOINT_PLUS, + FLOATINGPOINT_ADD, FLOATINGPOINT_SUB, FLOATINGPOINT_MULT, FLOATINGPOINT_DIV, diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index a5c7af161..28506d0bd 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -19,10 +19,11 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H #include <map> -#include "options/main_options.h" -#include "theory/quantifiers/sygus/sygus_unif.h" +#include "options/main_options.h" #include "theory/quantifiers/lazy_trie.h" +#include "theory/quantifiers/sygus/sygus_unif.h" +#include "util/bool.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 0c9cb91d7..746cc7f11 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -20,8 +20,10 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" -#include "theory/strings/word.h" #include "theory/rewriter.h" +#include "theory/strings/word.h" +#include "util/bitvector.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 1fc685992..3201bb2c8 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -24,11 +24,10 @@ namespace cvc5 { class TConvProofGenerator; class ProofNodeManager; +class TrustNode; namespace theory { -class TrustNode; - namespace builtin { class BuiltinProofRuleChecker; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 22b77c4fb..6d1b9955a 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -18,6 +18,7 @@ #include <map> #include "base/map_util.h" +#include "expr/emptyset.h" #include "expr/kind.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" @@ -32,6 +33,7 @@ #include "theory/sep/theory_sep_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" +#include "util/cardinality.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 8e6cd08c6..afd860288 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -15,10 +15,12 @@ * \todo document this file */ -#include "expr/attribute.h" #include "theory/sep/theory_sep_rewriter.h" -#include "theory/quantifiers/quant_util.h" + +#include "expr/attribute.h" +#include "expr/emptyset.h" #include "options/sep_options.h" +#include "theory/quantifiers/quant_util.h" namespace cvc5 { namespace theory { diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index ec5abfacc..063c440a5 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -25,6 +25,8 @@ #include "theory/sets/normal_form.h" #include "theory/theory_model.h" #include "theory/valuation.h" +#include "util/cardinality.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 0f15727e0..4bde524f7 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -16,10 +16,11 @@ properties check presolve # constants constant EMPTYSET \ - ::cvc5::EmptySet \ - ::cvc5::EmptySetHashFunction \ - "expr/emptyset.h" \ - "the empty set constant; payload is an instance of the cvc5::EmptySet class" + class \ + EmptySet \ + ::cvc5::EmptySetHashFunction \ + "expr/emptyset.h" \ + "the empty set constant; payload is an instance of the cvc5::EmptySet class" # the type operator SET_TYPE 1 "set type, takes as parameter the type of the elements" @@ -42,10 +43,11 @@ operator SUBSET 2 "subset predicate; first parameter a subset of second operator MEMBER 2 "set membership predicate; first parameter a member of second" constant SINGLETON_OP \ - ::cvc5::SingletonOp \ - ::cvc5::SingletonOpHashFunction \ - "theory/sets/singleton_op.h" \ - "operator for singletons; payload is an instance of the cvc5::SingletonOp class" + class \ + SingletonOp \ + ::cvc5::SingletonOpHashFunction \ + "theory/sets/singleton_op.h" \ + "operator for singletons; payload is an instance of the cvc5::SingletonOp class" parameterized SINGLETON SINGLETON_OP 1 \ "constructs a set of a single element. First parameter is a SingletonOp. Second is a term" diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 930f7da86..eb839e1c0 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -18,6 +18,8 @@ #ifndef CVC5__THEORY__SETS__NORMAL_FORM_H #define CVC5__THEORY__SETS__NORMAL_FORM_H +#include "expr/emptyset.h" + namespace cvc5 { namespace theory { namespace sets { diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index fad14bb71..42e317402 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -26,6 +26,7 @@ #include "theory/sets/normal_form.h" #include "theory/sets/theory_sets.h" #include "theory/theory_model.h" +#include "util/rational.h" #include "util/result.h" using namespace std; diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 69780b04c..0546c7f95 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -18,6 +18,7 @@ #include "expr/skolem_manager.h" #include "theory/sets/theory_sets.h" #include "theory/sets/theory_sets_private.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index d05318cc8..14b5c6d52 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -20,6 +20,7 @@ #include "options/sets_options.h" #include "theory/sets/normal_form.h" #include "theory/sets/rels_utils.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp index 503a33ebd..8c395a958 100644 --- a/src/theory/sets/theory_sets_type_enumerator.cpp +++ b/src/theory/sets/theory_sets_type_enumerator.cpp @@ -15,6 +15,8 @@ #include "theory/sets/theory_sets_type_enumerator.h" +#include "util/bitvector.h" + namespace cvc5 { namespace theory { namespace sets { diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index 232865994..91c592f18 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -19,6 +19,8 @@ #include <sstream> #include "theory/sets/normal_form.h" +#include "theory/sets/singleton_op.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index b9c331acc..0e17f50a9 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -300,7 +300,7 @@ bool SharedTermsDatabase::isKnown(TNode literal) const { } } -theory::TrustNode SharedTermsDatabase::explain(TNode literal) const +TrustNode SharedTermsDatabase::explain(TNode literal) const { if (d_pfee != nullptr) { diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index b684ff56f..4e09ac23f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -186,7 +186,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj { /** * Returns an explanation of the propagation that came from the database. */ - theory::TrustNode explain(TNode literal) const; + TrustNode explain(TNode literal) const; /** * Add an equality to propagate. diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 4c3b2f17e..66e3cf634 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -22,6 +22,7 @@ #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" #include "theory/theory.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 6ee88b298..00491128a 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -21,6 +21,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index a6e4ce698..fb1d086a4 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -16,6 +16,7 @@ #include "theory/strings/core_solver.h" #include "base/configuration.h" +#include "expr/sequence.h" #include "options/strings_options.h" #include "smt/logic_exception.h" #include "theory/rewriter.h" @@ -23,6 +24,8 @@ #include "theory/strings/strings_entail.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 3dbb6b89b..94d99732a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -20,6 +20,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 30ca92808..743a5c006 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -57,10 +57,11 @@ enumerator STRING_TYPE \ "theory/strings/type_enumerator.h" constant CONST_STRING \ - ::cvc5::String \ - ::cvc5::strings::StringHashFunction \ - "util/string.h" \ - "a string of characters" + class \ + String \ + ::cvc5::strings::StringHashFunction \ + "util/string.h" \ + "a string of characters" # the type operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements" @@ -76,10 +77,11 @@ enumerator SEQUENCE_TYPE \ "theory/strings/type_enumerator.h" constant CONST_SEQUENCE \ - ::cvc5::Sequence \ - ::cvc5::SequenceHashFunction \ - "expr/sequence.h" \ - "a sequence of characters" + class \ + Sequence \ + ::cvc5::SequenceHashFunction \ + "expr/sequence.h" \ + "a sequence of characters" operator SEQ_UNIT 1 "a sequence of length one" operator SEQ_NTH 2 "The nth element of a sequence" @@ -101,17 +103,19 @@ operator REGEXP_EMPTY 0 "regexp empty" operator REGEXP_SIGMA 0 "regexp all characters" constant REGEXP_REPEAT_OP \ - ::cvc5::RegExpRepeat \ - ::cvc5::RegExpRepeatHashFunction \ - "util/regexp.h" \ - "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class" + struct \ + RegExpRepeat \ + ::cvc5::RegExpRepeatHashFunction \ + "util/regexp.h" \ + "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class" parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term" constant REGEXP_LOOP_OP \ - ::cvc5::RegExpLoop \ - ::cvc5::RegExpLoopHashFunction \ - "util/regexp.h" \ - "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class" + struct \ + RegExpLoop \ + ::cvc5::RegExpLoopHashFunction \ + "util/regexp.h" \ + "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class" parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term" #internal diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index c3580d963..ac0e487f9 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -20,6 +20,8 @@ #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; @@ -90,7 +92,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // into fixed length regular expressions are easy to handle. // the index of _* in re unsigned pivotIndex = 0; - size_t numPivotIndex = 0; + bool hasPivotIndex = false; + bool hasFixedLength = true; std::vector<Node> childLengths; std::vector<Node> childLengthsPostPivot; for (unsigned i = 0, size = children.size(); i < size; i++) @@ -99,34 +102,34 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node fl = RegExpEntail::getFixedLengthForRegexp(c); if (fl.isNull()) { - if (numPivotIndex == 0 && c.getKind() == REGEXP_STAR + if (!hasPivotIndex && c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_SIGMA) { - numPivotIndex = 1; + hasPivotIndex = true; pivotIndex = i; // zero is used in sum below and is used for concat-fixed-len fl = zero; } else { - numPivotIndex++; + hasFixedLength = false; } } if (!fl.isNull()) { childLengths.push_back(fl); - if (numPivotIndex > 0) + if (hasPivotIndex) { childLengthsPostPivot.push_back(fl); } } } - Node lenSum = childLengths.size() > 1 ? nm->mkNode(PLUS, childLengths) - : childLengths[0]; - // if we have at most one pivot index - if (numPivotIndex <= 1) + Node lenSum = childLengths.size() > 1 + ? nm->mkNode(PLUS, childLengths) + : (childLengths.empty() ? zero : childLengths[0]); + // if we have a fixed length + if (hasFixedLength) { - bool hasPivotIndex = (numPivotIndex == 1); Assert(re.getNumChildren() == children.size()); std::vector<Node> conc; conc.push_back(nm->mkNode(hasPivotIndex ? GEQ : EQUAL, lenx, lenSum)); diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index b789db6a4..3d4a2d143 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -18,6 +18,8 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 96351cda9..106ce09d0 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -23,6 +23,7 @@ #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/regexp.h" using namespace cvc5::kind; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 91cea5fe8..7ef1242c6 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -25,7 +25,10 @@ #include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/regexp.h" #include "util/statistics_registry.h" +#include "util/string.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index e5e014f9d..1ddf2af58 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -18,6 +18,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index a5d01eefd..a527d99dc 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -21,6 +21,8 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp index f5ccc3bef..9bb6a2420 100644 --- a/src/theory/strings/strings_fmf.cpp +++ b/src/theory/strings/strings_fmf.cpp @@ -15,6 +15,8 @@ #include "theory/strings/strings_fmf.h" +#include "util/rational.h" + using namespace std; using namespace cvc5::context; using namespace cvc5::kind; diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 41a8ac448..b455d8a9b 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -19,6 +19,7 @@ #include "expr/node_builder.h" #include "theory/strings/theory_strings_utils.h" #include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index c6710fb73..c7b3b5300 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -23,6 +23,8 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 3da682871..83a4fa04a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -24,7 +24,9 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/word.h" +#include "util/rational.h" #include "util/statistics_registry.h" +#include "util/string.h" using namespace cvc5; using namespace cvc5::kind; diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index a7e891d86..183344aa2 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -19,6 +19,7 @@ #include "expr/node_manager.h" #include "expr/sequence.h" #include "options/strings_options.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index ed610ca95..c763557ca 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -22,6 +22,9 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/strings_entail.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/regexp.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 1f2f31a61..5641312cb 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -15,6 +15,7 @@ #include "theory/strings/type_enumerator.h" +#include "expr/sequence.h" #include "theory/strings/theory_strings_utils.h" #include "util/string.h" diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index e2a81f54a..02fa85faa 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -19,6 +19,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 676351dd5..85cd7e6b3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -810,7 +810,7 @@ theory::Theory::PPAssertStatus TheoryEngine::solve( return solveStatus; } -theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq) +TrustNode TheoryEngine::ppRewriteEquality(TNode eq) { Assert(eq.getKind() == kind::EQUAL); std::vector<SkolemLemma> lems; @@ -1297,7 +1297,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The } } -void TheoryEngine::lemma(theory::TrustNode tlemma, +void TheoryEngine::lemma(TrustNode tlemma, theory::LemmaProperty p, theory::TheoryId atomsTo, theory::TheoryId from) @@ -1368,7 +1368,7 @@ void TheoryEngine::lemma(theory::TrustNode tlemma, d_lemmasAdded = true; } -void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId) +void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) { Assert(tconflict.getKind() == TrustNodeKind::CONFLICT); TNode conflict = tconflict.getNode(); @@ -1486,7 +1486,7 @@ void TheoryEngine::setIncomplete(theory::TheoryId theory, d_incompleteId = id; } -theory::TrustNode TheoryEngine::getExplanation( +TrustNode TheoryEngine::getExplanation( std::vector<NodeTheoryPair>& explanationVector) { Assert(explanationVector.size() == 1); @@ -1788,7 +1788,7 @@ theory::TrustNode TheoryEngine::getExplanation( return trn; } - return theory::TrustNode::mkTrustPropExp(conclusion, expNode, nullptr); + return TrustNode::mkTrustPropExp(conclusion, expNode, nullptr); } bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ffcaf392f..f293a2cc8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -191,7 +191,7 @@ class TheoryEngine { * generator (if it exists), * @param theoryId The theory that sent the conflict */ - void conflict(theory::TrustNode conflict, theory::TheoryId theoryId); + void conflict(TrustNode conflict, theory::TheoryId theoryId); /** * Debugging flag to ensure that shutdown() is called before the @@ -272,7 +272,7 @@ class TheoryEngine { * @param atomsTo the theory that atoms of the lemma should be sent to * @param from the theory that sent the lemma */ - void lemma(theory::TrustNode node, + void lemma(TrustNode node, theory::LemmaProperty p, theory::TheoryId atomsTo = theory::THEORY_LAST, theory::TheoryId from = theory::THEORY_LAST); @@ -422,8 +422,7 @@ class TheoryEngine { * where the node is the one to be explained, and the theory is the * theory that sent the literal. */ - theory::TrustNode getExplanation( - std::vector<NodeTheoryPair>& explanationVector); + TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector); /** Are proofs enabled? */ bool isProofEnabled() const; @@ -433,7 +432,7 @@ class TheoryEngine { * Preprocess rewrite equality, called by the preprocessor to rewrite * equalities appearing in the input. */ - theory::TrustNode ppRewriteEquality(TNode eq); + TrustNode ppRewriteEquality(TNode eq); /** Notify (preprocessed) assertions. */ void notifyPreprocessedAssertions(const std::vector<Node>& assertions); @@ -477,8 +476,7 @@ class TheoryEngine { * take this proof into account (when proofs are enabled). */ theory::Theory::PPAssertStatus solve( - theory::TrustNode tliteral, - theory::TrustSubstitutionMap& substitutionOut); + TrustNode tliteral, theory::TrustSubstitutionMap& substitutionOut); /** * Preregister a Theory atom with the responsible theory (or @@ -540,7 +538,7 @@ class TheoryEngine { /** * Returns an explanation of the node propagated to the SAT solver. */ - theory::TrustNode getExplanation(TNode node); + TrustNode getExplanation(TNode node); /** * Get the pointer to the model object used by this theory engine. diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index f10716bd9..073accdae 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -30,21 +30,21 @@ TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, d_false = NodeManager::currentNM()->mkConst(false); } -theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain( +TrustNode TheoryEngineProofGenerator::mkTrustExplain( TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf) { Node p; - theory::TrustNode trn; + TrustNode trn; if (lit == d_false) { // propagation of false is a conflict - trn = theory::TrustNode::mkTrustConflict(exp, this); + trn = TrustNode::mkTrustConflict(exp, this); p = trn.getProven(); Assert(p.getKind() == NOT); } else { - trn = theory::TrustNode::mkTrustPropExp(lit, exp, this); + trn = TrustNode::mkTrustPropExp(lit, exp, this); p = trn.getProven(); Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2); } diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index ab0f616fe..68f7dea32 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -53,9 +53,9 @@ class TheoryEngineProofGenerator : public ProofGenerator * explanation already exists, then the previous explanation is taken, which * also suffices for proving the implication. */ - theory::TrustNode mkTrustExplain(TNode lit, - Node exp, - std::shared_ptr<LazyCDProof> lpf); + TrustNode mkTrustExplain(TNode lit, + Node exp, + std::shared_ptr<LazyCDProof> lpf); /** * Get proof for, which expects implications corresponding to explained * propagations (=> exp lit) registered by the above method. This currently diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index dd1e0b883..8eec7f911 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "theory/rewriter.h" #include "theory/trust_substitutions.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 951a62cae..4034e43bd 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -26,6 +26,7 @@ #include "theory/type_enumerator.h" #include "theory/type_set.h" #include "theory/uf/equality_engine.h" +#include "util/cardinality.h" namespace cvc5 { diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 0a038845c..e3e197953 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -16,6 +16,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" +#include "expr/uninterpreted_constant.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index aaeea6a4f..97bf7aaac 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -22,6 +22,7 @@ #include "base/exception.h" #include "expr/node.h" #include "expr/type_node.h" +#include "util/integer.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 166df3c80..5b919860e 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -28,6 +28,7 @@ #include "theory/theory_model.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index f81abdca1..e95c8963e 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -18,6 +18,8 @@ #include <climits> #include <sstream> +#include "util/rational.h" + namespace cvc5 { namespace theory { namespace uf { |