| /dports/math/cvc4/CVC4-1.7/src/theory/booleans/ |
| H A D | theory_bool.cpp | 34 Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { in ppAssert() argument
45 outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false)); in ppAssert()
51 outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true)); in ppAssert()
56 return Theory::ppAssert(in, outSubstitutions); in ppAssert()
|
| H A D | theory_bool.h | 36 PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sets/ |
| H A D | theory_sets.cpp | 88 Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { in ppAssert() argument
89 return d_internal->ppAssert( in, outSubstitutions ); in ppAssert()
|
| H A D | theory_sets.h | 56 PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
|
| H A D | theory_sets_private.h | 259 Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
|
| H A D | theory_sets_private.cpp | 2225 Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { in ppAssert() argument
2240 outSubstitutions.addSubstitution(in[0], in[1]); in ppAssert()
2250 outSubstitutions.addSubstitution(in[1], in[0]); in ppAssert()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | theory_arith.cpp | 77 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { in ppAssert() argument
78 return d_internal->ppAssert(in, outSubstitutions); in ppAssert()
|
| H A D | theory_arith.h | 82 PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
|
| H A D | theory_arith_private.h | 452 Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
|
| H A D | theory_arith_private.cpp | 1321 Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { in ppAssert() argument
1380 outSubstitutions.addSubstitution(minVar, elim); in ppAssert()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory.cpp | 289 SubstitutionMap& outSubstitutions) in ppAssert() argument
300 outSubstitutions.addSubstitution(in[0], in[1]); in ppAssert()
306 outSubstitutions.addSubstitution(in[1], in[0]); in ppAssert()
|
| H A D | theory.h | 557 virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | theory_bv.cpp | 661 SubstitutionMap& outSubstitutions) in ppAssert() argument
670 outSubstitutions.addSubstitution(in[0], in[1]); in ppAssert()
676 outSubstitutions.addSubstitution(in[1], in[0]); in ppAssert()
721 outSubstitutions.addSubstitution(extract[0], concat); in ppAssert()
|
| H A D | theory_bv.h | 103 PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.h | 78 PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
|
| H A D | theory_sep.cpp | 92 Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { in ppAssert() argument
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.h | 179 PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
|
| H A D | theory_arrays.cpp | 349 Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { in ppAssert() argument
358 outSubstitutions.addSubstitution(in[0], in[1]); in ppAssert()
364 outSubstitutions.addSubstitution(in[1], in[0]); in ppAssert()
|