diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/datatypes/sygus_extension.cpp | 37 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/model_engine.h | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 3 | ||||
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 30 |
6 files changed, 25 insertions, 65 deletions
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 24288216f..d962ad189 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -130,39 +130,10 @@ void SygusExtension::assertFact( Node n, bool polarity, std::vector< Node >& lem Node SygusExtension::getTermOrderPredicate( Node n1, Node n2 ) { NodeManager* nm = NodeManager::currentNM(); std::vector< Node > comm_disj; - // (1) size of left is greater than size of right - Node sz_less = - nm->mkNode(GT, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); - comm_disj.push_back( sz_less ); - // (2) ...or sizes are equal and first child is less by term order - std::vector<Node> sz_eq_cases; - Node sz_eq = - nm->mkNode(EQUAL, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); - sz_eq_cases.push_back( sz_eq ); - if( options::sygusOpt1() ){ - TypeNode tnc = n1.getType(); - const DType& cdt = tnc.getDType(); - for( unsigned j=0; j<cdt.getNumConstructors(); j++ ){ - std::vector<Node> case_conj; - for (unsigned k = 0; k < j; k++) - { - case_conj.push_back(utils::mkTester(n2, k, cdt).negate()); - } - if (!case_conj.empty()) - { - Node corder = nm->mkNode( - OR, - utils::mkTester(n1, j, cdt).negate(), - case_conj.size() == 1 ? case_conj[0] : nm->mkNode(AND, case_conj)); - sz_eq_cases.push_back(corder); - } - } - } - Node sz_eqc = sz_eq_cases.size() == 1 ? sz_eq_cases[0] - : nm->mkNode(kind::AND, sz_eq_cases); - comm_disj.push_back( sz_eqc ); - - return nm->mkNode(kind::OR, comm_disj); + // size of left is greater than or equal to the size of right + Node szGeq = + nm->mkNode(GEQ, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); + return szGeq; } void SygusExtension::registerTerm( Node n, std::vector< Node >& lemmas ) { diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 5b2931e42..4012f687f 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -163,11 +163,6 @@ void ModelEngine::assertNode( Node f ){ } -bool ModelEngine::optOneQuantPerRound(){ - return options::fmfOneQuantPerRound(); -} - - int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); @@ -230,7 +225,8 @@ int ModelEngine::checkModel(){ //determine if we should check this quantifier if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){ exhaustiveInstantiate( q, e ); - if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ + if (d_quantEngine->inConflict()) + { break; } }else{ diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index b39dd03f8..3165b01db 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -29,9 +29,6 @@ class ModelEngine : public QuantifiersModule { friend class RepSetIterator; private: - //options - bool optOneQuantPerRound(); -private: //check model int checkModel(); //exhaustively instantiate quantifier (possibly using mbqi) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index f81d2455c..2e5a834b1 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -556,12 +556,9 @@ Node CegSingleInv::reconstructToSyntax(Node s, }else{ Trace("csi-sol") << "Post-process solution..." << std::endl; Node prev = d_solution; - if (options::minSynthSol()) - { - d_solution = - d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite( - d_solution); - } + d_solution = + d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite( + d_solution); if( prev!=d_solution ){ Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl; } diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 3ef3a3edc..57fe40517 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -136,8 +136,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, bool addedEvalLemmas = false; // Refinement evaluation should not be done for grammars with symbolic // constructors. - bool doRefEval = options::sygusRefEval() && !d_usingSymCons; - if (doRefEval) + if (!d_usingSymCons) { Trace("cegqi-engine") << " *** Do refinement lemma evaluation" << (doGen ? " with conjecture-specific refinement" diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index e2cafa4d3..723a8c08e 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1484,22 +1484,22 @@ bool CoreSolver::detectLoop(NormalForm& nfi, unsigned rproc) { int has_loop[2] = { -1, -1 }; - if( options::stringLB() != 2 ) { - for( unsigned r=0; r<2; r++ ) { - NormalForm& nf = r == 0 ? nfi : nfj; - NormalForm& nfo = r == 0 ? nfj : nfi; - std::vector<Node>& nfv = nf.d_nf; - std::vector<Node>& nfov = nfo.d_nf; - if (!nfov[index].isConst()) + for (unsigned r = 0; r < 2; r++) + { + NormalForm& nf = r == 0 ? nfi : nfj; + NormalForm& nfo = r == 0 ? nfj : nfi; + std::vector<Node>& nfv = nf.d_nf; + std::vector<Node>& nfov = nfo.d_nf; + if (nfov[index].isConst()) + { + continue; + } + for (unsigned lp = index + 1, lpEnd = nfv.size() - rproc; lp < lpEnd; lp++) + { + if (nfv[lp] == nfov[index]) { - for (unsigned lp = index + 1; lp < nfv.size() - rproc; lp++) - { - if (nfv[lp] == nfov[index]) - { - has_loop[r] = lp; - break; - } - } + has_loop[r] = lp; + break; } } } |