diff options
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 49954c111..9346970d1 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -18,13 +18,14 @@ #include "theory/sets/theory_sets_private.h" #include "expr/emptyset.h" +#include "expr/node_algorithm.h" #include "options/sets_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/sets/theory_sets.h" +#include "theory/quantifiers/term_database.h" #include "theory/sets/normal_form.h" +#include "theory/sets/theory_sets.h" #include "theory/theory_model.h" #include "util/result.h" -#include "theory/quantifiers/term_database.h" #define AJR_IMPLEMENTATION @@ -2200,28 +2201,37 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou //this is based off of Theory::ppAssert Node var; - if (in.getKind() == kind::EQUAL) { - if (in[0].isVar() && !in[1].hasSubterm(in[0]) && - (in[1].getType()).isSubtypeOf(in[0].getType()) ){ - if( !in[0].getType().isSet() || !options::setsExt() ){ + if (in.getKind() == kind::EQUAL) + { + if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]) + && (in[1].getType()).isSubtypeOf(in[0].getType())) + { + if (!in[0].getType().isSet() || !options::setsExt()) + { outSubstitutions.addSubstitution(in[0], in[1]); var = in[0]; status = Theory::PP_ASSERT_STATUS_SOLVED; } - }else if (in[1].isVar() && !in[0].hasSubterm(in[1]) && - (in[0].getType()).isSubtypeOf(in[1].getType())){ - if( !in[1].getType().isSet() || !options::setsExt() ){ + } + else if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]) + && (in[0].getType()).isSubtypeOf(in[1].getType())) + { + if (!in[1].getType().isSet() || !options::setsExt()) + { outSubstitutions.addSubstitution(in[1], in[0]); var = in[1]; status = Theory::PP_ASSERT_STATUS_SOLVED; } - }else if (in[0].isConst() && in[1].isConst()) { - if (in[0] != in[1]) { + } + else if (in[0].isConst() && in[1].isConst()) + { + if (in[0] != in[1]) + { status = Theory::PP_ASSERT_STATUS_CONFLICT; } } } - + if( status==Theory::PP_ASSERT_STATUS_SOLVED ){ Trace("sets-var-elim") << "Sets : ppAssert variable eliminated : " << in << ", var = " << var << std::endl; /* |