diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 13:35:53 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-12-14 13:35:53 -0600 |
commit | e16ab44a2b4622bb5745633cbafd43a0023a518c (patch) | |
tree | d980bdc3dc771abfc8101036d1e2aaebc8020134 /src/theory/quantifiers/relevant_domain.cpp | |
parent | ad34df900d79aad64558b354a866870715bfd007 (diff) | |
parent | effb0d47ba5bfaebae17dcd06153489dccd90eff (diff) |
Merge branch 'master' into cav22-stringscav22-strings
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 0f3699990..f0684f04a 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" +#include "util/rational.h" using namespace cvc5::kind; @@ -301,6 +302,7 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) { if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){ + NodeManager* nm = NodeManager::currentNM(); RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n]; rdl.d_merge = false; int varCount = 0; @@ -405,10 +407,14 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No if( ( !hasPol || pol ) && n[0].getType().isInteger() ){ if( n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ - rdl.d_val.push_back(ArithMSum::offset(r_add, i == 0 ? 1 : -1)); + Node roff = nm->mkNode( + PLUS, r_add, nm->mkConstInt(Rational(i == 0 ? 1 : -1))); + rdl.d_val.push_back(roff); } }else if( n.getKind()==GEQ ){ - rdl.d_val.push_back(ArithMSum::offset(r_add, varLhs ? 1 : -1)); + Node roff = nm->mkNode( + PLUS, r_add, nm->mkConstInt(Rational(varLhs ? 1 : -1))); + rdl.d_val.push_back(roff); } } } |