diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 11:28:25 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 11:28:25 -0400 |
commit | b01a91bb5690b2648a5b8d91f940a6746cba34a3 (patch) | |
tree | 9c4881ead1f7bce2bdd522765a648b6ed896d5c3 /src/theory/quantifiers | |
parent | 3fc61e7f2b84765dc547634463198b30516ed432 (diff) | |
parent | 698f5a09b1c0177abfd2eaa2b110de100fd108ef (diff) |
Merge remote-tracking branch 'upstream/master' into sets
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/modes.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/modes.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 33 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 |
9 files changed, 48 insertions, 32 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index d815e0ee8..098a7819a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -648,7 +648,18 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); Node curr; for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { - Node v = getRepresentative( d_models[op]->d_value[i] ); + Node v = d_models[op]->d_value[i]; + if( !hasTerm( v ) ){ + //can happen when the model basis term does not exist in ground assignment + TypeNode tn = v.getType(); + if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){ + //see full_model_check.cpp line 366 + v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ]; + }else{ + Assert( false ); + } + } + v = getRepresentative( v ); if( curr.isNull() ){ curr = v; }else{ @@ -656,6 +667,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node cond = d_models[op]->d_cond[i]; std::vector< Node > children; for( unsigned j=0; j<cond.getNumChildren(); j++) { + TypeNode tn = vars[j].getType(); if (isInterval(cond[j])){ if( !isStar(cond[j][0]) ){ children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) ); @@ -663,7 +675,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { if( !isStar(cond[j][1]) ){ children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) ); } - }else if (!isStar(cond[j])){ + }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground eqc of this type + d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){ Node c = getUsedRepresentative( cond[j] ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); } @@ -673,6 +686,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); } } + Trace("fmc-model") << "Made " << curr << " for " << op << std::endl; curr = Rewriter::rewrite( curr ); return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 3b6c8e492..0f3e53827 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n void FullModelChecker::doNegate( Def & dc ) { for (unsigned i=0; i<dc.d_cond.size(); i++) { if (!dc.d_value[i].isNull()) { - dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true; + dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i] ); } } } diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp index 10185914e..8bd97a8a7 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -79,8 +79,8 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { switch(mode) { - case theory::quantifiers::MBQI_DEFAULT: - out << "MBQI_DEFAULT"; + case theory::quantifiers::MBQI_GEN_EVAL: + out << "MBQI_GEN_EVAL"; break; case theory::quantifiers::MBQI_NONE: out << "MBQI_NONE"; @@ -94,6 +94,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) case theory::quantifiers::MBQI_INTERVAL: out << "MBQI_INTERVAL"; break; + case theory::quantifiers::MBQI_TRUST: + out << "MBQI_TRUST"; + break; default: out << "MbqiMode!UNKNOWN"; } diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 89e10b175..80534c8b0 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -58,13 +58,13 @@ typedef enum { } AxiomInstMode; typedef enum { - /** default, mbqi from CADE 24 paper */ - MBQI_DEFAULT, + /** mbqi from CADE 24 paper */ + MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, /** implementation that mimics inst-gen */ MBQI_INST_GEN, - /** mbqi from Section 5.4.2 of AJR thesis */ + /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, /** mbqi with integer intervals */ MBQI_FMC_INTERVAL, diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 0865f2c0b..e733764f0 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -67,11 +67,13 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation +option instMaxLevel --inst-max-level=N int :default -1 + maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly -option fullSaturateQuant --full-saturate-quant bool :default true +option fullSaturateQuant --full-saturate-quant bool :default false when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" @@ -95,7 +97,7 @@ option internalReps /--disable-quant-internal-reps bool :default true option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write use finite model finding heuristic for quantifier instantiation -option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" +option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false only add one instantiation per quantifier per round for mbqi @@ -112,7 +114,7 @@ option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding -option fmfBoundInt --fmf-bound-int bool :default false :read-write +option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write finite model finding on bounded integer quantification option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e9c754d4a..b7e624a66 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -82,8 +82,8 @@ static const std::string mbqiModeHelp = "\ Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ \n\ default \n\ -+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper.\n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ + Modulo Theories.\n\ \n\ none \n\ + Disable model-based quantifier instantiation.\n\ @@ -91,12 +91,12 @@ none \n\ instgen \n\ + Use instantiation algorithm that mimics Inst-Gen calculus. \n\ \n\ -fmc \n\ -+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ - Modulo Theories.\n\ +gen-ev \n\ ++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper based on generalizing evaluations.\n\ \n\ fmc-interval \n\ -+ Same as fmc, but with intervals for models of integer functions.\n\ ++ Same as default, but with intervals for models of integer functions.\n\ \n\ interval \n\ + Use algorithm that abstracts domain elements as intervals. \n\ @@ -131,9 +131,6 @@ conflict \n\ partial \n\ + Apply QCF algorithm to instantiate heuristically as well. \n\ \n\ -partial \n\ -+ Apply QCF to instantiate heuristically as well. \n\ -\n\ mc \n\ + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ \n\ @@ -217,21 +214,21 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar } inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return MBQI_DEFAULT; - } else if(optarg == "none") { + if(optarg == "gen-ev") { + return MBQI_GEN_EVAL; + } else if(optarg == "none") { return MBQI_NONE; - } else if(optarg == "instgen") { + } else if(optarg == "instgen") { return MBQI_INST_GEN; - } else if(optarg == "fmc") { + } else if(optarg == "default" || optarg == "fmc") { return MBQI_FMC; - } else if(optarg == "fmc-interval") { + } else if(optarg == "fmc-interval") { return MBQI_FMC_INTERVAL; - } else if(optarg == "interval") { + } else if(optarg == "interval") { return MBQI_INTERVAL; - } else if(optarg == "trust") { + } else if(optarg == "trust") { return MBQI_TRUST; - } else if(optarg == "help") { + } else if(optarg == "help") { puts(mbqiModeHelp.c_str()); exit(1); } else { diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index c0b318f23..e27d438be 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { bool MatchGen::isHandledUfTerm( TNode n ) {
return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
- n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;
+ n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
}
Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cf183dd18..3168d21a0 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) { } d_par_op_map[op][tn1][tn2] = n; return n; - }else if( n.getKind()==APPLY_UF ){ + }else if( inst::Trigger::isAtomicTrigger( n ) ){ return n.getOperator(); }else{ return Node::null(); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 6912c9e89..3de12b9c9 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ bool Trigger::isAtomicTrigger( Node n ){ return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER; + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; } bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ |