diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-28 16:21:08 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-28 16:21:08 -0600 |
commit | c0d75b9ead289143749bcd030e390e614d4658e5 (patch) | |
tree | 717abec4197ad9284ec76250434dba11e523cfa5 | |
parent | 2731897b5f9ed46c66e3bdf20cde47ef43923a9c (diff) |
Fixes for cbqi (#1453)
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 40 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 |
2 files changed, 22 insertions, 20 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 877db6797..78cd77c6e 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -1160,15 +1160,6 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) } } -struct sortCegVarOrder { - bool operator() (Node i, Node j) { - TypeNode it = i.getType(); - TypeNode jt = j.getType(); - return ( it!=jt && jt.isSubtypeOf( it ) ) || ( it==jt && i<j ); - } -}; - - void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl; d_input_vars.clear(); @@ -1245,29 +1236,40 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st Trace("cbqi-debug") << "Determine variable order..." << std::endl; if (!d_vars.empty()) { - TypeNode tn0 = d_vars[0].getType(); - bool doSort = false; std::map<Node, unsigned> voo; - for (unsigned i = 0; i < d_vars.size(); i++) + bool doSort = false; + std::vector<Node> vars; + std::map<TypeNode, std::vector<Node> > tvars; + for (unsigned i = 0, size = d_vars.size(); i < size; i++) { voo[d_vars[i]] = i; d_var_order_index.push_back(0); - if (d_vars[i].getType() != tn0) + TypeNode tn = d_vars[i].getType(); + if (tn.isInteger()) { doSort = true; + tvars[tn].push_back(d_vars[i]); + } + else + { + vars.push_back(d_vars[i]); } } if (doSort) { Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl; - sortCegVarOrder scvo; - std::sort(d_vars.begin(), d_vars.end(), scvo); + for (std::pair<const TypeNode, std::vector<Node> >& vs : tvars) + { + vars.insert(vars.end(), vs.second.begin(), vs.second.end()); + } + Trace("cbqi-debug") << "Consider variables in this order : " << std::endl; - for (unsigned i = 0; i < d_vars.size(); i++) + for (unsigned i = 0; i < vars.size(); i++) { - d_var_order_index[voo[d_vars[i]]] = i; - Trace("cbqi-debug") << " " << d_vars[i] << " : " << d_vars[i].getType() - << ", index was : " << voo[d_vars[i]] << std::endl; + d_var_order_index[voo[vars[i]]] = i; + Trace("cbqi-debug") << " " << vars[i] << " : " << vars[i].getType() + << ", index was : " << voo[vars[i]] << std::endl; + d_vars[i] = vars[i]; } Trace("cbqi-debug") << std::endl; } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 2d97bd160..609b6e461 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -400,7 +400,7 @@ bool Trigger::isCbqiKind( Kind k ) { }else{ //CBQI typically works for satisfaction-complete theories TheoryId t = kindToTheoryId( k ); - return t==THEORY_BV || t==THEORY_DATATYPES; + return t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL; } } |