type = "bool"
default = "true"
help = "sygus symmetry breaking lemmas based on pbe conjectures"
-
-[[option]]
- name = "sygusOpt1"
- category = "regular"
- long = "sygus-opt1"
- type = "bool"
- default = "false"
- read_only = true
- help = "sygus experimental option"
[[option]]
name = "sygusSymBreakLazy"
default = "false"
help = "only add one instantiation per quantifier per round for mbqi"
-[[option]]
- name = "fmfOneQuantPerRound"
- category = "regular"
- long = "mbqi-one-quant-per-round"
- type = "bool"
- default = "false"
- read_only = true
- help = "only add instantiations for one quantifier per round for mbqi"
-
[[option]]
name = "mbqiInterleave"
category = "regular"
default = "false"
help = "use instantiation engine in conjunction with finite model finding"
-[[option]]
- name = "fmfInstGen"
- category = "regular"
- long = "fmf-inst-gen"
- type = "bool"
- default = "true"
- read_only = true
- help = "enable Inst-Gen instantiation techniques for finite model finding"
-
-[[option]]
- name = "fmfInstGenOneQuantPerRound"
- category = "regular"
- long = "fmf-inst-gen-one-quant-per-round"
- type = "bool"
- default = "false"
- read_only = true
- help = "only perform Inst-Gen instantiation techniques on one quantifier per round"
-
[[option]]
name = "fmfFreshDistConst"
category = "regular"
default = "false"
help = "do not consider instances of quantified formulas that are currently true in model, if it is available"
-[[option]]
- name = "instPropagate"
- category = "regular"
- long = "inst-prop"
- type = "bool"
- default = "false"
- help = "internal propagation for instantiations for selecting relevant instances"
-
[[option]]
name = "qcfEagerTest"
category = "regular"
read_only = true
help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
-### Rewrite rules options
-
-[[option]]
- name = "rrOneInstPerRound"
- category = "regular"
- long = "rr-one-inst-per-round"
- type = "bool"
- default = "false"
- read_only = true
- help = "add one instance of rewrite rule per round"
-
### Induction options
[[option]]
read_only = true
help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
-[[option]]
- name = "sygusRefEval"
- category = "regular"
- long = "sygus-ref-eval"
- type = "bool"
- default = "true"
- read_only = true
- help = "direct evaluation of refinement lemmas for conflict analysis"
-
[[option]]
name = "sygusStream"
category = "regular"
name = "trust"
help = "Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures."
-[[option]]
- name = "minSynthSol"
- category = "regular"
- long = "min-synth-sol"
- type = "bool"
- default = "true"
- help = "Minimize synthesis solutions"
-
[[option]]
name = "sygusEvalOpt"
category = "regular"
default = "false"
help = "experimental features in the theory of strings"
-[[option]]
- name = "stringLB"
- smt_name = "strings-lb"
- category = "regular"
- long = "strings-lb=N"
- type = "unsigned"
- default = "0"
- predicates = ["unsignedLessEqual2"]
- read_only = true
- help = "the strategy of LB rule application: 0-lazy, 1-eager, 2-no"
-
[[option]]
name = "stdPrintASCII"
category = "regular"
read_only = true
help = "strings eager check"
-[[option]]
- name = "stringEIT"
- category = "regular"
- long = "strings-eit"
- type = "bool"
- default = "false"
- read_only = true
- help = "the eager intersection used by the theory of strings"
-
[[option]]
name = "stringIgnNegMembership"
category = "regular"
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 ) {
}
-bool ModelEngine::optOneQuantPerRound(){
- return options::fmfOneQuantPerRound();
-}
-
-
int ModelEngine::checkModel(){
FirstOrderModel* fm = d_quantEngine->getModel();
//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{
class ModelEngine : public QuantifiersModule
{
friend class RepSetIterator;
-private:
- //options
- bool optOneQuantPerRound();
private:
//check model
int checkModel();
}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;
}
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"
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;
}
}
}
projects / cvc5.git / commitdiff