diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-20 10:37:32 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-20 10:37:46 -0600 |
commit | f37804c3da98f4eb1888991fd8b7157437aeeb44 (patch) | |
tree | 0baeed78ff7107a2f8ac32d8b2a8cc3d6e10de91 /src/smt | |
parent | 531ec6e52b75cd2f600a3fc781383e7539f2335a (diff) |
Fix ite and iff handling in QCF. Add option for heuristic instantiation in QCF (not working yet). Improve automatic option setting for quantifiers.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7ada9d350..4ab8cb548 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1185,10 +1185,13 @@ void SmtEngine::setLogicInternal() throw() { } } if ( options::fmfBoundInt() ){ + //must have finite model finding on + options::finiteModelFind.set( true ); if( options::mbqiMode()!=quantifiers::MBQI_NONE && + options::mbqiMode()!=quantifiers::MBQI_FMC && options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){ - //if bounded integers are set, must use full model check for MBQI - options::mbqiMode.set( quantifiers::MBQI_FMC ); + //if bounded integers are set, use no MBQI by default + options::mbqiMode.set( quantifiers::MBQI_NONE ); } } if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ @@ -1198,6 +1201,9 @@ void SmtEngine::setLogicInternal() throw() { if( options::ufssSymBreak() ){ options::sortInference.set( true ); } + if( options::qcfMode.wasSetByUser() ){ + options::quantConflictFind.set( true ); + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ @@ -1572,13 +1578,13 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF argTypes.push_back(NodeManager::currentNM()->stringType()); argTypes.push_back(NodeManager::currentNM()->integerType()); argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", + d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->stringType()), "uf substr", NodeManager::SKOLEM_EXACT_NAME); } - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] ); Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero); @@ -1595,13 +1601,13 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF argTypes.push_back(NodeManager::currentNM()->stringType()); argTypes.push_back(NodeManager::currentNM()->integerType()); argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", + d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->stringType()), "uf substr", NodeManager::SKOLEM_EXACT_NAME); } - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); |