diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/util | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 2 | ||||
-rw-r--r-- | src/util/datatype.h | 6 | ||||
-rw-r--r-- | src/util/ite_removal.cpp | 39 | ||||
-rw-r--r-- | src/util/options.cpp | 176 | ||||
-rw-r--r-- | src/util/options.h | 120 |
5 files changed, 316 insertions, 27 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index f009bbbbe..86a43c878 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -438,7 +438,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, d_tester = em->mkVar(d_name.substr(d_name.find('\0') + 1), em->mkTesterType(self)); d_name.resize(d_name.find('\0')); d_constructor = em->mkVar(d_name, em->mkConstructorType(*this, self)); - //associate constructor with all selectors + // associate constructor with all selectors for(iterator i = begin(), i_end = end(); i != i_end; ++i) { (*i).d_constructor = d_constructor; } diff --git a/src/util/datatype.h b/src/util/datatype.h index d39d7110d..b701073c7 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -361,9 +361,9 @@ public: * * Datatypes may also be defined parametrically, such as this example: * - * DATATYPE
- * list[T] = cons(car : T, cdr : list[T]) | null,
- * tree = node(children : list[tree]) | leaf
+ * DATATYPE + * list[T] = cons(car : T, cdr : list[T]) | null, + * tree = node(children : list[tree]) | leaf * END; * * Here, the definition of the parametric datatype list, where T is a type variable. diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 9d2524170..9a4fc8dc2 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -79,23 +79,30 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, } // If not an ITE, go deep - vector<Node> newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Remove the ITEs from the children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, iteSkolemMap); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } + if( node.getKind() != kind::FORALL && + node.getKind() != kind::EXISTS && + node.getKind() != kind::REWRITE_RULE ) { + vector<Node> newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Remove the ITEs from the children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = run(*it, output, iteSkolemMap); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } - // If changes, we rewrite - if(somethingChanged) { - cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); - nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite); - return cachedRewrite; + // If changes, we rewrite + if(somethingChanged) { + cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); + nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite); + return cachedRewrite; + } else { + nodeManager->setAttribute(node, IteRewriteAttr(), Node::null()); + return node; + } } else { nodeManager->setAttribute(node, IteRewriteAttr(), Node::null()); return node; diff --git a/src/util/options.cpp b/src/util/options.cpp index 26881e052..1296fa5af 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -130,6 +130,25 @@ Options::Options() : arithRewriteEqSetByUser(false), ufSymmetryBreaker(false), ufSymmetryBreakerSetByUser(false), + miniscopeQuant(true), + miniscopeQuantFreeVar(true), + prenexQuant(true), + varElimQuant(false), + cnfQuant(false), + preSkolemQuant(false), + smartTriggers(true), + registerQuantBodyTerms(false), + instWhenMode(INST_WHEN_FULL_LAST_CALL), + eagerInstQuant(false), + finiteModelFind(false), + fmfRegionSat(false), + fmfModelBasedInst(true), + efficientEMatching(false), + literalMatchMode(LITERAL_MATCH_NONE), + cbqi(false), + cbqiSetByUser(false), + userPatternsQuant(true), + flipDecision(false), lemmaOutputChannel(NULL), lemmaInputChannel(NULL), threads(2),// default should be 1 probably, but say 2 for now @@ -240,6 +259,27 @@ Additional CVC4 options:\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\ CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ + --disable-miniscope-quant disable miniscope quantifiers\n\ + --disable-miniscope-quant-fv disable miniscope quantifiers for ground subformulas\n\ + --disable-prenex-quant disable prenexing of quantified formulas\n\ + --var-elim-quant enable variable elimination of quantified formulas\n\ + --cnf-quant apply CNF conversion to quantified formulas\n\ + --pre-skolem-quant apply skolemization eagerly to bodies of quantified formulas\n\ + --disable-smart-triggers disable smart triggers\n\ + --register-quant-body-terms consider terms within bodies of quantified formulas for matching\n\ + --inst-when=MODE when to apply instantiation\n\ + --eager-inst-quant apply quantifier instantiation eagerly\n\ + --finite-model-find use finite model finding heuristic for quantifier instantiation\n\ + --use-fmf-region-sat use region-based SAT heuristic for finite model finding\n\ + --disable-fmf-model-inst disable model-based instantiation for finite model finding\n\ + --efficient-e-matching use efficient E-matching\n\ + --literal-matching=MODE choose literal matching mode\n\ + --enable-cbqi turns on counterexample-based quantifier instantiation [off by default]\n\ + --disable-cbqi turns off counterexample-based quantifier instantiation\n\ + --ignore-user-patterns ignore user-provided patterns for quantifier instantiation\n\ + --enable-flip-decision turns on flip decision heuristic\n\ + --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ + --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\ --threads=N sets the number of solver threads\n\ --threadN=string configures thread N (0..#threads-1)\n\ --filter-lemma-length=N don't share lemmas strictly longer than N\n\ @@ -439,7 +479,7 @@ void Options::printLanguageHelp(std::ostream& out) { */ enum OptionValue { OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */ - SMTCOMP, + SMTCOMP, STATS, SEGV_NOSPIN, OUTPUT_LANGUAGE, @@ -496,6 +536,25 @@ enum OptionValue { DISABLE_ARITHMETIC_REWRITE_EQUALITIES, ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, + DISABLE_MINISCOPE_QUANT, + DISABLE_MINISCOPE_QUANT_FV, + DISABLE_PRENEX_QUANT, + VAR_ELIM_QUANT, + CNF_QUANT, + PRE_SKOLEM_QUANT, + DISABLE_SMART_TRIGGERS, + REGISTER_QUANT_BODY_TERMS, + INST_WHEN, + EAGER_INST_QUANT, + FINITE_MODEL_FIND, + FMF_REGION_SAT, + DISABLE_FMF_MODEL_BASED_INST, + EFFICIENT_E_MATCHING, + LITERAL_MATCHING, + ENABLE_CBQI, + DISABLE_CBQI, + IGNORE_USER_PATTERNS, + ENABLE_FLIP_DECISION, PARALLEL_THREADS, PARALLEL_SEPARATE_OUTPUT, PORTFOLIO_FILTER_LENGTH, @@ -602,6 +661,25 @@ static struct option cmdlineOptions[] = { { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES }, { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, + { "disable-miniscope-quant", no_argument, NULL, DISABLE_MINISCOPE_QUANT }, + { "disable-miniscope-quant-fv", no_argument, NULL, DISABLE_MINISCOPE_QUANT_FV }, + { "disable-prenex-quant", no_argument, NULL, DISABLE_PRENEX_QUANT }, + { "var-elim-quant", no_argument, NULL, VAR_ELIM_QUANT }, + { "cnf-quant", no_argument, NULL, CNF_QUANT }, + { "pre-skolem-quant", no_argument, NULL, PRE_SKOLEM_QUANT }, + { "disable-smart-triggers", no_argument, NULL, DISABLE_SMART_TRIGGERS }, + { "register-quant-body-terms", no_argument, NULL, REGISTER_QUANT_BODY_TERMS }, + { "inst-when", required_argument, NULL, INST_WHEN }, + { "eager-inst-quant", no_argument, NULL, EAGER_INST_QUANT }, + { "finite-model-find", no_argument, NULL, FINITE_MODEL_FIND }, + { "use-fmf-region-sat", no_argument, NULL, FMF_REGION_SAT }, + { "disable-fmf-model-inst", no_argument, NULL, DISABLE_FMF_MODEL_BASED_INST }, + { "efficient-e-matching", no_argument, NULL, EFFICIENT_E_MATCHING }, + { "literal-matching", required_argument, NULL, LITERAL_MATCHING }, + { "enable-cbqi", no_argument, NULL, ENABLE_CBQI }, + { "disable-cbqi", no_argument, NULL, DISABLE_CBQI }, + { "ignore-user-patterns", no_argument, NULL, IGNORE_USER_PATTERNS }, + { "enable-flip-decision", no_argument, NULL, ENABLE_FLIP_DECISION }, { "threads", required_argument, NULL, PARALLEL_THREADS }, { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT }, { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH }, @@ -984,7 +1062,7 @@ throw(OptionException) { case 'm': produceModels = true; break; - + case PRODUCE_ASSIGNMENTS: produceAssignments = true; break; @@ -1016,7 +1094,7 @@ throw(OptionException) { throw OptionException("This is not a proof-enabled build of CVC4; --proof cannot be used"); #endif /* CVC4_PROOF */ break; - + case NO_TYPE_CHECKING: typeChecking = false; earlyTypeChecking = false; @@ -1073,7 +1151,91 @@ throw(OptionException) { ufSymmetryBreaker = false; ufSymmetryBreakerSetByUser = true; break; - + case DISABLE_MINISCOPE_QUANT: + miniscopeQuant = false; + break; + case DISABLE_MINISCOPE_QUANT_FV: + miniscopeQuantFreeVar = false; + break; + case DISABLE_PRENEX_QUANT: + prenexQuant = false; + break; + case VAR_ELIM_QUANT: + varElimQuant = true; + break; + case CNF_QUANT: + cnfQuant = true; + break; + case PRE_SKOLEM_QUANT: + preSkolemQuant = true; + break; + case DISABLE_SMART_TRIGGERS: + smartTriggers = false; + break; + case REGISTER_QUANT_BODY_TERMS: + registerQuantBodyTerms = true; + break; + case INST_WHEN: + if(!strcmp(optarg, "pre-full")) { + instWhenMode = INST_WHEN_PRE_FULL; + } else if(!strcmp(optarg, "full")) { + instWhenMode = INST_WHEN_FULL; + } else if(!strcmp(optarg, "full-last-call")) { + instWhenMode = INST_WHEN_FULL_LAST_CALL; + } else if(!strcmp(optarg, "last-call")) { + instWhenMode = INST_WHEN_LAST_CALL; + } else if(!strcmp(optarg, "help")) { + //puts(instWhenHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --inst-when: `") + + optarg + "'. Try --inst-when help."); + } + break; + case EAGER_INST_QUANT: + eagerInstQuant = true; + break; + case FINITE_MODEL_FIND: + finiteModelFind = true; + break; + case FMF_REGION_SAT: + fmfRegionSat = true; + break; + case DISABLE_FMF_MODEL_BASED_INST: + fmfModelBasedInst = false; + break; + case EFFICIENT_E_MATCHING: + efficientEMatching = true; + break; + case LITERAL_MATCHING: + if(!strcmp(optarg, "none")) { + literalMatchMode = LITERAL_MATCH_NONE; + } else if(!strcmp(optarg, "predicate")) { + literalMatchMode = LITERAL_MATCH_PREDICATE; + } else if(!strcmp(optarg, "equality")) { + literalMatchMode = LITERAL_MATCH_EQUALITY; + } else if(!strcmp(optarg, "help")) { + //puts(literalMatchHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --literal-matching: `") + + optarg + "'. Try --literal-matching help."); + } + break; + case ENABLE_CBQI: + cbqi = true; + cbqiSetByUser = true; + break; + case DISABLE_CBQI: + cbqi = false; + cbqiSetByUser = true; + break; + case IGNORE_USER_PATTERNS: + userPatternsQuant = false; + break; + case ENABLE_FLIP_DECISION: + flipDecision = true; + break; case TIME_LIMIT: { int i = atoi(optarg); @@ -1141,7 +1303,7 @@ throw(OptionException) { optarg + "' is not between 0.0 and 1.0."); } break; - + case SAT_RESTART_FIRST: { int i = atoi(optarg); @@ -1151,7 +1313,7 @@ throw(OptionException) { satRestartFirst = i; break; } - + case SAT_RESTART_INC: { int i = atoi(optarg); @@ -1341,7 +1503,7 @@ throw(OptionException) { case PORTFOLIO_FILTER_LENGTH: sharingFilterByLength = atoi(optarg); - break; + break; case ':': // This can be a long or short option, and the way to get at the name of it is different. diff --git a/src/util/options.h b/src/util/options.h index 0584fdc2a..fb5f71060 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -310,6 +310,126 @@ struct CVC4_PUBLIC Options { */ bool ufSymmetryBreakerSetByUser; + /** + * Whether to mini-scope quantifiers. + * For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to + * ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) + */ + bool miniscopeQuant; + + /** + * Whether to mini-scope quantifiers based on formulas with no free variables. + * For example, forall x. ( P( x ) V Q ) will be rewritten to + * ( forall x. P( x ) ) V Q + */ + bool miniscopeQuantFreeVar; + + /** + * Whether to prenex (nested universal) quantifiers + */ + bool prenexQuant; + + /** + * Whether to variable-eliminate quantifiers. + * For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to + * forall y. P( c, y ) + */ + bool varElimQuant; + + /** + * Whether to CNF quantifier bodies + */ + bool cnfQuant; + + /** + * Whether to pre-skolemize quantifier bodies. + * For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to + * forall x. P( x ) => f( S( x ) ) = x + */ + bool preSkolemQuant; + + /** + * Whether to use smart triggers + */ + bool smartTriggers; + + /** + * Whether to consider terms in the bodies of quantifiers for matching + */ + bool registerQuantBodyTerms; + + /** Enumeration of inst_when modes (when to instantiate). */ + typedef enum { + /** Apply instantiation round before full effort (possibly at standard effort) */ + INST_WHEN_PRE_FULL, + /** Apply instantiation round at full effort or above */ + INST_WHEN_FULL, + /** Apply instantiation round at full effort half the time, and last call always */ + INST_WHEN_FULL_LAST_CALL, + /** Apply instantiation round at last call only */ + INST_WHEN_LAST_CALL, + } InstWhenMode; + /** When to perform instantiation round. */ + InstWhenMode instWhenMode; + + /** + * Whether to eagerly instantiate quantifiers + */ + bool eagerInstQuant; + + /** + * Whether to use finite model find heuristic + */ + bool finiteModelFind; + + /** + * Whether to use region-based SAT for finite model finding + */ + bool fmfRegionSat; + + /** + * Whether to use model-based exhaustive instantiation for finite model finding + */ + bool fmfModelBasedInst; + + /** + * Whether to use efficient E-matching + */ + bool efficientEMatching; + + /** Enumeration of literal matching modes. */ + typedef enum { + /** Do not consider polarity of patterns */ + LITERAL_MATCH_NONE, + /** Consider polarity of boolean predicates only */ + LITERAL_MATCH_PREDICATE, + /** Consider polarity of boolean predicates, as well as equalities */ + LITERAL_MATCH_EQUALITY, + } LiteralMatchMode; + + /** Which literal matching mode to use. */ + LiteralMatchMode literalMatchMode; + + /** + * Whether to do counterexample-based quantifier instantiation + */ + bool cbqi; + + /** + * Whether the user explicitly requested that counterexample-based + * quantifier instantiation be enabled or disabled. + */ + bool cbqiSetByUser; + + /** + * Whether to use user patterns for pattern-based instantiation + */ + bool userPatternsQuant; + + /** + * Whether to use flip decision (useful when cbqi=true) + */ + bool flipDecision; /** The output channel to receive notfication events for new lemmas */ LemmaOutputChannel* lemmaOutputChannel; |