summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/run-script-casc25-tfn5
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp5
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.h2
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp4
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp16
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.h2
-rw-r--r--src/theory/quantifiers/term_database.cpp1
8 files changed, 29 insertions, 8 deletions
diff --git a/contrib/run-script-casc25-tfn b/contrib/run-script-casc25-tfn
index d3c5d0344..6888d7b49 100644
--- a/contrib/run-script-casc25-tfn
+++ b/contrib/run-script-casc25-tfn
@@ -15,7 +15,7 @@ echo "------- cvc4-tfn casc 25 : $bench at $2..."
function trywith {
limit=$1; shift;
echo "--- Run $@ at $limit...";
- (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null |
+ (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench) 2>/dev/null |
(read w1 w2 w3 result w4 w5;
case "$result" in
Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
@@ -25,11 +25,10 @@ function trywith {
}
function finishwith {
echo "--- Run $@...";
- $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench
+ $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench
}
trywith 30 --cbqi2 --decision=internal --full-saturate-quant
-trywith 60 --finite-model-find --sort-inference --uf-ss-fair
trywith 30 --cbqi --full-saturate-quant
trywith 60 --cbqi --cbqi-recurse --full-saturate-quant
trywith 60 --fmf-bound-int --macros-quant
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6fdfadbd3..54c97750a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3272,7 +3272,7 @@ void SmtEnginePrivate::processAssertions() {
}
}
dumpAssertions("post-skolem-quant", d_assertions);
- if( options::macrosQuant() ){
+ if( options::macrosQuant() && !options::incrementalSolving() ){
//quantifiers macro expansion
bool success;
do{
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 22ffcd278..8e7e3d69c 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -706,7 +706,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
*/
}
-void CegInstantiator::check() {
+bool CegInstantiator::check() {
for( unsigned r=0; r<2; r++ ){
std::vector< Node > subs;
@@ -716,10 +716,11 @@ void CegInstantiator::check() {
std::vector< int > subs_typ;
//try to add an instantiation
if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){
- return;
+ return true;
}
}
Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+ return false;
}
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 54f762720..eb99fc4f6 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -72,7 +72,7 @@ public:
//delta
Node d_n_delta;
//check : add instantiations based on valuation of d_vars
- void check();
+ bool check();
// get delta lemmas : on-demand force minimality of d_n_delta
void getDeltaLemmas( std::vector< Node >& lems );
};
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index fdb64f6b0..da3c0cce0 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1717,15 +1717,18 @@ void TermGenEnv::collectSignatureInformation() {
for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
if( !getTermDatabase()->d_op_map[it->first].empty() ){
Node nn = getTermDatabase()->d_op_map[it->first][0];
+ Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
bool do_enum = true;
//check if we have enumerated ground terms
if( nn.getKind()==APPLY_UF ){
+ Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl;
if( !d_cg->hasEnumeratedUf( nn ) ){
do_enum = false;
}
}
if( do_enum ){
+ Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl;
d_funcs.push_back( it->first );
for( unsigned i=0; i<nn.getNumChildren(); i++ ){
d_func_args[it->first].push_back( nn[i].getType() );
@@ -1738,6 +1741,7 @@ void TermGenEnv::collectSignatureInformation() {
getTermDatabase()->computeUfEqcTerms( it->first );
}
}
+ Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl;
}
}
//shuffle functions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index cbf0dbbd9..de80146f9 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -369,6 +369,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( q
void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
d_check_delta_lemma = true;
+ d_check_delta_lemma_lc = true;
}
int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
@@ -383,6 +384,9 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" );
Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
d_quantEngine->getOutputChannel().lemma( delta_lem );
+ d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
+ Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub );
+ d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
}
cinst->d_n_delta = d_n_delta;
for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
@@ -412,8 +416,18 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
}
Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
d_curr_quant = f;
- cinst->check();
+ bool addedLemma = cinst->check();
d_curr_quant = Node::null();
+ return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
+ }else if( e==3 ){
+ if( d_check_delta_lemma_lc ){
+ d_check_delta_lemma_lc = false;
+ d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub );
+ d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub );
+ Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl;
+ Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub );
+ d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+ }
}
return STATUS_UNKNOWN;
}
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 586cd492c..13e8cf54b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -100,8 +100,10 @@ private:
CegqiOutputInstStrategy * d_out;
std::map< Node, CegInstantiator * > d_cinst;
Node d_n_delta;
+ Node d_n_delta_ub;
Node d_curr_quant;
bool d_check_delta_lemma;
+ bool d_check_delta_lemma_lc;
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
int process( Node f, Theory::Effort effort, int e );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 8c99881d6..189866494 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -945,6 +945,7 @@ Node TermDb::getSkolemizedBody( Node f ){
}
Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
+ Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl;
std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );
unsigned teIndex;
if( it==d_typ_enum_map.end() ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback