From 8ebd49cb903ba19f9330820d02af08e226c9b791 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 10 May 2014 15:14:34 -0500 Subject: [PATCH] Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, minor changes. --- contrib/run-script-cascj7-fof | 6 +- contrib/run-script-cascj7-tff | 29 ++++ src/smt/smt_engine.cpp | 3 + src/theory/quantifiers/ambqi_builder.cpp | 82 ++++----- src/theory/quantifiers/inst_strategy_cbqi.cpp | 158 +++++++++++------- src/theory/quantifiers/inst_strategy_cbqi.h | 5 +- src/theory/quantifiers/options | 2 +- .../regress0/quantifiers/ARI176e1.smt2 | 5 + test/regress/regress0/quantifiers/Makefile.am | 3 +- 9 files changed, 185 insertions(+), 108 deletions(-) create mode 100755 contrib/run-script-cascj7-tff create mode 100755 test/regress/regress0/quantifiers/ARI176e1.smt2 diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof index bfaaf722f..151413ac2 100755 --- a/contrib/run-script-cascj7-fof +++ b/contrib/run-script-cascj7-fof @@ -25,9 +25,9 @@ function trywith { if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } -trywith 30 -trywith 10 --decision=internal +trywith 30 --full-saturate-quant +trywith 10 --decision=internal --full-saturate-quant trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev trywith 15 --finite-model-find --decision=justification-stoponly -trywith $to --quant-cf +trywith $to --quant-cf --full-saturate-quant echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff new file mode 100755 index 000000000..445f7b08a --- /dev/null +++ b/contrib/run-script-cascj7-tff @@ -0,0 +1,29 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 150" + +file=${bench##*/} +filename=${file%.*} + +# use: trywith [params..] +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in +# which case this run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $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 +} + +trywith 30 --full-saturate-quant +trywith 120 --quant-cf --qcf-tconstraint --full-saturate-quant +trywith $to --cbqi --cbqi-recurse --full-saturate-quant --flip-decision +echo "% SZS status" "GaveUp for $filename" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1397c10d3..5d6a913b0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1174,6 +1174,9 @@ void SmtEngine::setDefaults() { //must have finite model finding on options::finiteModelFind.set( true ); } + if( options::recurseCbqi() ){ + options::cbqi.set( true ); + } if( options::fmfBoundInt() ){ //must have finite model finding on options::finiteModelFind.set( true ); diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 0b75c4a77..c6a5f4227 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -15,7 +15,7 @@ #include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/term_database.h" - +#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; @@ -148,48 +148,52 @@ void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsign } bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) { - if( d_value==1 ){ - //instantiations are all true : ignore this - return true; - }else{ - if( depth==q[0].getNumChildren() ){ - if( qe->addInstantiation( q, terms ) ){ - Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl; - inst++; - return true; - }else{ - Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl; - //we are incomplete - return false; - } + if( inst==0 || !options::fmfOneInstPerRound() ){ + if( d_value==1 ){ + //instantiations are all true : ignore this + return true; }else{ - bool osuccess = true; - TypeNode tn = m->getVariable( q, depth ).getType(); - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - //get witness term - unsigned index = 0; - bool success; - do { - success = false; - index = getId( it->first, index ); - if( index<32 ){ - Assert( indexd_rep_set.d_type_reps[tn].size() ); - terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index]; - //terms[depth] = m->d_rep_set.d_type_reps[tn][index]; - if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){ - //if we are incomplete, and have not yet added an instantiation, keep trying - index++; - Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl; - }else{ - success = true; + if( depth==q[0].getNumChildren() ){ + if( qe->addInstantiation( q, terms ) ){ + Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl; + inst++; + return true; + }else{ + Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl; + //we are incomplete + return false; + } + }else{ + bool osuccess = true; + TypeNode tn = m->getVariable( q, depth ).getType(); + for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ + //get witness term + unsigned index = 0; + bool success; + do { + success = false; + index = getId( it->first, index ); + if( index<32 ){ + Assert( indexd_rep_set.d_type_reps[tn].size() ); + terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index]; + //terms[depth] = m->d_rep_set.d_type_reps[tn][index]; + if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){ + //if we are incomplete, and have not yet added an instantiation, keep trying + index++; + Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl; + }else{ + success = true; + } } - } - }while( !success && index<32 ); - //mark if we are incomplete - osuccess = osuccess && success; + }while( !success && index<32 ); + //mark if we are incomplete + osuccess = osuccess && success; + } + return osuccess; } - return osuccess; } + }else{ + return true; } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index f9b4dd588..fef6b38d1 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -34,6 +34,7 @@ using namespace CVC4::theory::datatypes; InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategy( ie ), d_th( th ), d_counter( 0 ){ d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); + d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); } bool InstStrategySimplex::calculateShouldProcess( Node f ){ @@ -65,36 +66,33 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ArithVariables::var_iterator vi, vend; for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ ArithVar x = *vi; - if( d_th->d_internal->d_partialModel.hasEitherBound( x ) ){ - Node n = avnm.asNode(x); - - //collect instantiation constants - std::vector< Node > ics; - getInstantiationConstants( n, ics ); - for( unsigned i=0; i t(kind::PLUS); - if( n.getKind()==PLUS ){ - for( int j=0; j<(int)n.getNumChildren(); j++ ){ - addTermToRow( ics[i], x, n[j], t ); - } - }else{ - addTermToRow( ics[i], x, n, t ); - } - d_instRows[ics[i]].push_back( x ); - //this theory has constraints from f - Node f = TermDb::getInstConstAttr(ics[i]); - Debug("quant-arith") << "Has constraints from " << f << std::endl; - //set that we should process it - d_quantActive[ f ] = true; - //set tableaux term - if( t.getNumChildren()==0 ){ - d_tableaux_term[ics[i]][x] = NodeManager::currentNM()->mkConst( Rational(0) ); - }else if( t.getNumChildren()==1 ){ - d_tableaux_term[ics[i]][x] = t.getChild( 0 ); - }else{ - d_tableaux_term[ics[i]][x] = t; + //collect instantiation constants + std::vector< Node > ics; + getInstantiationConstants( n, ics ); + for( unsigned i=0; i t(kind::PLUS); + if( n.getKind()==PLUS ){ + for( int j=0; j<(int)n.getNumChildren(); j++ ){ + addTermToRow( ics[i], x, n[j], t ); } + }else{ + addTermToRow( ics[i], x, n, t ); + } + d_instRows[ics[i]].push_back( x ); + //this theory has constraints from f + Node f = TermDb::getInstConstAttr(ics[i]); + Debug("quant-arith") << "Has constraints from " << f << std::endl; + //set that we should process it + d_quantActive[ f ] = true; + //set tableaux term + if( t.getNumChildren()==0 ){ + d_tableaux_term[ics[i]][x] = d_zero; + }else if( t.getNumChildren()==1 ){ + d_tableaux_term[ics[i]][x] = t.getChild( 0 ); + }else{ + d_tableaux_term[ics[i]][x] = t; } } } @@ -134,26 +132,50 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ if( e<2 ){ return STATUS_UNFINISHED; }else if( e==2 ){ - //Notice() << f << std::endl; - //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl; - //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl; + //the point instantiation + InstMatch m_point( f ); + bool m_point_valid = true; + int lem = 0; + //scan over all instantiation rows for( int i=0; igetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; for( int j=0; j<(int)d_instRows[ic].size(); j++ ){ ArithVar x = d_instRows[ic][j]; if( !d_ceTableaux[ic][x].empty() ){ - Debug("quant-arith-simplex") << "Check row " << ic << " " << x << std::endl; + if( Debug.isOn("quant-arith-simplex") ){ + Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl; + Debug("quant-arith-simplex") << " "; + for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){ + if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } + Debug("quant-arith-simplex") << it->first << " * " << it->second; + } + Debug("quant-arith-simplex") << " = "; + Node v = getTableauxValue( x, false ); + Debug("quant-arith-simplex") << v << std::endl; + Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl; + Debug("quant-arith-simplex") << " ce-term : "; + for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){ + if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } + Debug("quant-arith-simplex") << it->first << " * " << it->second; + } + Debug("quant-arith-simplex") << std::endl; + } //instantiation row will be A*e + B*t = beta, // where e is a vector of terms , and t is vector of ground terms. // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant // We will construct the term ( beta - B*t)/coeff to use for e_i. InstMatch m( f ); + for( unsigned k=0; kfirst; + //if it is integer, we need to find variable with coefficent +/- 1 if( var.getType().isInteger() ){ std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); - //try to find coefficent that is +/- 1 while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){ ++it; if( it==d_ceTableaux[ic][x].end() ){ @@ -162,28 +184,35 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ var = it->first; } } - //otherwise, try one that divides all ground term coefficients? DO_THIS + //Otherwise, try one that divides all ground term coefficients? + // Might be futile, if rewrite ensures gcd of coeffs is 1. } if( !var.isNull() ){ + //add to point instantiation if applicable + if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){ + Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl; + Node v = getTableauxValue( x, false ); + if( !var.getType().isInteger() || v.getType().isInteger() ){ + m_point.setValue( i, v ); + }else{ + m_point_valid = false; + } + } Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; - doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ); + if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){ + lem++; + } }else{ Debug("quant-arith-simplex") << "Could not find var." << std::endl; } - ////choose a new variable based on alternation strategy - //int index = d_counter%(int)d_th->d_ceTableaux[x].size(); - //Node var; - //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){ - // if( index==0 ){ - // var = it->first; - // break; - // } - // index--; - //} - //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var ); } } } + if( lem==0 && m_point_valid ){ + if( d_quantEngine->addInstantiation( f, m_point ) ){ + Debug("quant-arith-simplex") << "...added point instantiation." << std::endl; + } + } } return STATUS_UNKNOWN; } @@ -279,25 +308,30 @@ bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ // make term ( beta - term )/coeff + bool vIsInteger = var.getType().isInteger(); Node beta = getTableauxValue( x, minus_delta ); - Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); - if( !d_ceTableaux[ic][x][var].isNull() ){ - if( var.getType().isInteger() ){ - Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); - instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal ); - }else{ - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst() ); - instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); + if( !vIsInteger || beta.getType().isInteger() ){ + Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); + if( !d_ceTableaux[ic][x][var].isNull() ){ + if( vIsInteger ){ + Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); + instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal ); + }else{ + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst() ); + instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); + } } + instVal = Rewriter::rewrite( instVal ); + //use as instantiation value for var + int vn = var.getAttribute(InstVarNumAttribute()); + m.setValue( vn, instVal ); + Debug("quant-arith") << "Add instantiation " << m << std::endl; + return d_quantEngine->addInstantiation( f, m ); + }else{ + return false; } - instVal = Rewriter::rewrite( instVal ); - //use as instantiation value for var - int vn = var.getAttribute(InstVarNumAttribute()); - m.setValue( vn, instVal ); - Debug("quant-arith") << "Add instantiation " << m << std::endl; - return d_quantEngine->addInstantiation( f, m ); } - +/* Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){ if( d_th->d_internal->d_partialModel.hasArithVar(n) ){ ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n ); @@ -306,7 +340,7 @@ Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){ return NodeManager::currentNM()->mkConst( Rational(0) ); } } - +*/ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ const Rational& delta = d_th->d_internal->d_partialModel.getDelta(); DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v ); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index c70c90b29..a446c8b35 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -55,7 +55,7 @@ private: /** ce tableaux */ std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux; /** get value */ - Node getTableauxValue( Node n, bool minus_delta = false ); + //Node getTableauxValue( Node n, bool minus_delta = false ); Node getTableauxValue( arith::ArithVar v, bool minus_delta = false ); /** do instantiation */ bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var ); @@ -67,7 +67,8 @@ private: private: /** */ int d_counter; - /** negative one */ + /** constants */ + Node d_zero; Node d_negOne; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 38db10feb..f02a3bce1 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -82,7 +82,7 @@ option fullSaturateQuant --full-saturate-quant bool :default false 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" choose literal matching mode -option cbqi --enable-cbqi bool :default false +option cbqi --enable-cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default false diff --git a/test/regress/regress0/quantifiers/ARI176e1.smt2 b/test/regress/regress0/quantifiers/ARI176e1.smt2 new file mode 100755 index 000000000..dbeb96f29 --- /dev/null +++ b/test/regress/regress0/quantifiers/ARI176e1.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --cbqi-recurse +; EXPECT: unsat +(set-logic UFLIA) +(assert (forall ((U Int) (V Int)) (not (= (* 3 U) (+ 22 (* (- 5) V)))) ) ) +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index b21311da1..f12e67401 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -40,7 +40,8 @@ TESTS = \ qcft-javafe.filespace.TreeWalker.006.smt2 \ qcft-smtlib3dbc51.smt2 \ symmetric_unsat_7.smt2 \ - javafe.ast.StmtVec.009.smt2 + javafe.ast.StmtVec.009.smt2 \ + ARI176e1.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 -- 2.30.2