From: ajreynol Date: Sun, 10 May 2015 17:44:58 +0000 (+0200) Subject: Minor improvements to infrastructure. Minor changes to default options. Add tff scrip... X-Git-Tag: cvc5-1.0.0~6333 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0cb1add6db449c64c6ca63bc219761c8bc4a4de;p=cvc5.git Minor improvements to infrastructure. Minor changes to default options. Add tff script. Minor additions to sygus. --- diff --git a/contrib/run-script-casc25-fnt b/contrib/run-script-casc25-fnt index c53a0f26d..7f007186c 100644 --- a/contrib/run-script-casc25-fnt +++ b/contrib/run-script-casc25-fnt @@ -29,10 +29,10 @@ function finishwith { } # designed for 300 seconds -trywith 30 --finite-model-find --sort-inference --uf-ss-fair --mbqi=abs +trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev trywith 20 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair -trywith 20 --finite-model-find --decision=internal +trywith 20 --finite-model-find --decision=internal --sort-inference --uf-ss-fair trywith 20 --finite-model-find --uf-ss-totality --sort-inference --uf-ss-fair --mbqi=gen-ev -trywith 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev -finishwith --finite-model-find --quant-cf --sort-inference --uf-ss-fair --mbqi=abs +trywith 60 --finite-model-find --quant-cf --sort-inference --uf-ss-fair --mbqi=abs +finishwith --finite-model-find --sort-inference --uf-ss-fair --mbqi=abs # echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc25-fof b/contrib/run-script-casc25-fof index 3986b42f6..b6bea37dd 100755 --- a/contrib/run-script-casc25-fof +++ b/contrib/run-script-casc25-fof @@ -33,13 +33,13 @@ trywith 15 --relevant-triggers --clause-split --full-saturate-quant trywith 15 --clause-split --no-e-matching --full-saturate-quant trywith 15 --finite-model-find --quant-cf --sort-inference --uf-ss-fair trywith 5 --trigger-sel=max --full-saturate-quant -trywith 5 --multi-trigger-when-single --full-saturate-quant +trywith 5 --relevant-triggers --clause-split --multi-trigger-when-single --full-saturate-quant trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant trywith 5 --pre-skolem-quant --no-pre-skolem-quant-nested --full-saturate-quant -trywith 15 --decision=internal --full-saturate-quant -trywith 15 --no-quant-cf --full-saturate-quant -trywith 15 --trigger-sel=min --full-saturate-quant -trywith 30 --prenex-quant=none --full-saturate-quant +trywith 15 --relevant-triggers --decision=internal --full-saturate-quant +trywith 15 --clause-split --no-quant-cf --full-saturate-quant +trywith 15 --clause-split --trigger-sel=min --full-saturate-quant +trywith 30 --relevant-triggers --prenex-quant=none --full-saturate-quant trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev finishwith --term-db-mode=relevant --full-saturate-quant diff --git a/contrib/run-script-casc25-tff b/contrib/run-script-casc25-tff new file mode 100644 index 000000000..f6d244aad --- /dev/null +++ b/contrib/run-script-casc25-tff @@ -0,0 +1,38 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tff casc 25 : $bench at $2..." + +# use: trywith [params..] +# to attempt a run. If an SZS ontology result is printed, then +# the run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null | + (read w1 w2 w3 result w4 w5; + case "$result" in + Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} +function finishwith { + echo "--- Run $@..."; + $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench +} + +trywith 10 --cbqi2 --decision=internal --full-saturate-quant --force-logic="UFNIRA" +trywith 10 --relevant-triggers --full-saturate-quant --force-logic="UFNIRA" +trywith 20 --cbqi --cbqi-recurse --full-saturate-quant --force-logic="UFNIRA" +trywith 20 --no-e-matching --full-saturate-quant --force-logic="UFNIRA" +trywith 20 --qcf-tconstraint --full-saturate-quant --force-logic="UFNIRA" +trywith 70 --full-saturate-quant --force-logic="UFNIRA" +finishwith --cbqi2 --cbqi-recurse --full-saturate-quant --force-logic="UFNIRA" +# echo "% SZS status" "GaveUp for $filename" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6267a645e..b20b84690 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1430,6 +1430,9 @@ void SmtEngine::setDefaults() { if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } + if( !options::instNoEntail.wasSetByUser() ){ + options::instNoEntail.set( false ); + } } //implied options... diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index e1fc9e793..5e6bcf0b4 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -138,8 +138,8 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } -bool CegInstantiation::needsModel( Theory::Effort e ) { - return true; +unsigned CegInstantiation::needsModel( Theory::Effort e ) { + return QuantifiersEngine::QEFFORT_MODEL; } void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { @@ -543,8 +543,11 @@ void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) { } return; } + }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){ + out << n.getAttribute(SygusProxyAttribute()); + }else{ + out << n; } - out << n; } void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) { diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index f5077ad04..52e110720 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -118,7 +118,7 @@ public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); public: bool needsCheck( Theory::Effort e ); - bool needsModel( Theory::Effort e ); + unsigned needsModel( Theory::Effort e ); /* Call during quantifier engine's check */ void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 6e73b37a7..1d6676464 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -51,8 +51,8 @@ bool ModelEngine::needsCheck( Theory::Effort e ) { return e==Theory::EFFORT_LAST_CALL; } -bool ModelEngine::needsModel( Theory::Effort e ) { - return true; +unsigned ModelEngine::needsModel( Theory::Effort e ) { + return QuantifiersEngine::QEFFORT_MODEL; } void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 8c53084f0..6cdb47be2 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -48,7 +48,7 @@ public: virtual ~ModelEngine(); public: bool needsCheck( Theory::Effort e ); - bool needsModel( Theory::Effort e ); + unsigned needsModel( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node f ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index a529e37d0..4541c3d8a 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -166,7 +166,7 @@ option instNoEntail --inst-no-entail bool :read-write :default true ### rewrite rules options -option quantRewriteRules --rewrite-rules bool :default true +option quantRewriteRules --rewrite-rules bool :default false use rewrite rules module option rrOneInstPerRound --rr-one-inst-per-round bool :default false add one instance of rewrite rule per round @@ -207,6 +207,8 @@ option cegqiSingleInv --cegqi-si bool :default false process single invocation synthesis conjectures option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar +option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true + include constants when reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvAbort --cegqi-si-abort bool :default false abort if our synthesis conjecture is not single invocation diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e6f1ceee0..6c32ccb4a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1591,8 +1591,12 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) { sc = Node::fromExpr( dt[carg].getSygusOp() ); }else{ //TODO - - + if( !options::cegqiSingleInvReconstructConst() ){ + Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" ); + SygusProxyAttribute spa; + k.setAttribute(spa,c); + sc = k; + } } d_builtin_const_to_sygus[tn][c] = sc; return sc; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index db84ba885..37b1528b3 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -88,6 +88,10 @@ typedef expr::Attribute RrPriorityAttribute; struct LtePartialInstAttributeId {}; typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute; +// attribute for "contains instantiation constants from" +struct SygusProxyAttributeId {}; +typedef expr::Attribute SygusProxyAttribute; + class QuantifiersEngine; namespace inst{ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f6645c493..19e39d5b5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -44,6 +44,9 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; +unsigned QuantifiersModule::needsModel( Theory::Effort e ) { + return QuantifiersEngine::QEFFORT_NONE; +} eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { return d_quantEngine->getMasterEqualityEngine(); @@ -266,7 +269,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_ierCounter_lc++; } bool needsCheck = !d_lemmas_waiting.empty(); - bool needsModel = false; + unsigned needsModelE = QEFFORT_NONE; std::vector< QuantifiersModule* > qm; if( d_model->checkNeeded() ){ needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call @@ -274,9 +277,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_modules[i]->needsCheck( e ) ){ qm.push_back( d_modules[i] ); needsCheck = true; - if( d_modules[i]->needsModel( e ) ){ - needsModel = true; - } + unsigned me = d_modules[i]->needsModel( e ); + needsModelE = med_addedLemmas = 0; @@ -364,7 +365,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ break; //otherwise, complete the model generation if necessary - }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() ){ + }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() ){ Trace("quant-engine-debug") << "Build completed model..." << std::endl; d_builder->buildModel( d_model, true ); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 3ed6d369f..1d8c1591c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -55,9 +55,7 @@ public: /* whether this module needs to check this round */ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } /* whether this module needs a model built */ - virtual bool needsModel( Theory::Effort e ) { return false; } - /* whether this module needs a model built */ - virtual bool needsFullModel( Theory::Effort e ) { return false; } + virtual unsigned needsModel( Theory::Effort e ); /* reset at a round */ virtual void reset_round( Theory::Effort e ){} /* Call during quantifier engine's check */ @@ -143,6 +141,8 @@ public: //effort levels QEFFORT_CONFLICT, QEFFORT_STANDARD, QEFFORT_MODEL, + //none + QEFFORT_NONE, }; private: /** list of all quantifiers seen */ diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2 index 8fe88e9f5..f1506b3e8 100644 --- a/test/regress/regress0/push-pop/bug326.smt2 +++ b/test/regress/regress0/push-pop/bug326.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental +; COMMAND-LINE: --incremental --rewrite-rules (set-logic AUFLIA)