summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/run-script-casc25-fnt8
-rwxr-xr-xcontrib/run-script-casc25-fof10
-rw-r--r--contrib/run-script-casc25-tff38
-rw-r--r--src/smt/smt_engine.cpp3
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp9
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.h2
-rw-r--r--src/theory/quantifiers/model_engine.cpp4
-rw-r--r--src/theory/quantifiers/model_engine.h2
-rw-r--r--src/theory/quantifiers/options4
-rw-r--r--src/theory/quantifiers/term_database.cpp8
-rw-r--r--src/theory/quantifiers/term_database.h4
-rw-r--r--src/theory/quantifiers_engine.cpp15
-rw-r--r--src/theory/quantifiers_engine.h6
-rw-r--r--test/regress/regress0/push-pop/bug326.smt22
14 files changed, 85 insertions, 30 deletions
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<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
struct LtePartialInstAttributeId {};
typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
+// attribute for "contains instantiation constants from"
+struct SygusProxyAttributeId {};
+typedef expr::Attribute<SygusProxyAttributeId, Node> 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 = me<needsModelE ? me : needsModelE;
}
}
}
@@ -336,12 +338,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
}else if( e==Theory::EFFORT_FULL ){
++(d_statistics.d_instantiation_rounds);
}
-
Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){
bool success = true;
//build the model if any module requested it
- if( quant_e==QEFFORT_MODEL && needsModel ){
+ if( needsModelE==quant_e ){
Assert( d_builder!=NULL );
Trace("quant-engine-debug") << "Build model..." << std::endl;
d_builder->d_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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback