d_propEngine(NULL),
d_proofManager(NULL),
d_definedFunctions(NULL),
+ d_fmfRecFunctionsAbs(NULL),
+ d_fmfRecFunctionsConcrete(NULL),
d_assertionList(NULL),
d_assignments(NULL),
d_modelGlobalCommands(),
d_context->push();
d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
+ if( options::fmfFunWellDefined() ){
+ d_fmfRecFunctionsAbs = new(true) TypeNodeMap(d_userContext);
+ d_fmfRecFunctionsConcrete = new(true) NodeListMap(d_userContext);
+ }
d_modelCommands = new(true) smt::CommandList(d_userContext);
}
}
// otherwise expand it
- if (k == kind::APPLY && n.getOperator().getKind() != kind::LAMBDA) {
+ bool doExpand = ( k == kind::APPLY && n.getOperator().getKind() != kind::LAMBDA );
+ if( !doExpand ){
+ if( options::macrosQuant() ){
+ //expand if we have inferred an operator corresponds to a defined function
+ doExpand = k==kind::APPLY_UF && d_smt.isDefinedFunction( n.getOperator().toExpr() );
+ }
+ }
+ if (doExpand) {
// application of a user-defined symbol
TNode func = n.getOperator();
SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func);
}
}
dumpAssertions("post-skolem-quant", d_assertions);
- if( options::macrosQuant() && !options::incrementalSolving() ){
+ if( options::macrosQuant() ){
//quantifiers macro expansion
bool success;
do{
//fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
if( options::fmfFunWellDefined() ){
quantifiers::FunDefFmf fdf;
+ //must carry over current definitions (for incremental)
+ for( SmtEngine::TypeNodeMap::const_iterator fit = d_smt.d_fmfRecFunctionsAbs->begin(); fit != d_smt.d_fmfRecFunctionsAbs->end(); ++fit ){
+ Node f = (*fit).first;
+ TypeNode ft = (*fit).second;
+ fdf.d_sorts[f] = ft;
+ SmtEngine::NodeListMap::const_iterator fcit = d_smt.d_fmfRecFunctionsConcrete->find( f );
+ Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete->end() );
+ SmtEngine::NodeList* cl = (*fcit).second;
+ for( SmtEngine::NodeList::const_iterator cit = cl->begin(); cit != cl->end(); ++cit ){
+ fdf.d_input_arg_inj[f].push_back( *cit );
+ }
+ }
fdf.simplify( d_assertions.ref() );
+ //must store new definitions (for incremental)
+ for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
+ Node f = fdf.d_funcs[i];
+ d_smt.d_fmfRecFunctionsAbs->insert( f, fdf.d_sorts[f] );
+ SmtEngine::NodeList* cl = new(true) SmtEngine::NodeList( d_smt.d_userContext );
+ for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
+ cl->push_back( fdf.d_input_arg_inj[f][j] );
+ }
+ d_smt.d_fmfRecFunctionsConcrete->insert( f, cl );
+ }
}
}
typedef context::CDList<Expr> AssertionList;
/** The type of our internal assignment set */
typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
+ /** The types for the recursive function definitions */
+ typedef context::CDHashMap< Node, TypeNode, NodeHashFunction > TypeNodeMap;
+ typedef context::CDList<Node> NodeList;
+ typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
/** Expr manager context */
context::Context* d_context;
ProofManager* d_proofManager;
/** An index of our defined functions */
DefinedFunctionMap* d_definedFunctions;
+ /** recursive function definition abstractions for --fmf-fun */
+ TypeNodeMap* d_fmfRecFunctionsAbs;
+ NodeListMap* d_fmfRecFunctionsConcrete;
/**
* The assertion list (before any conversion) for supporting
Message() << "Cannot define function " << f << " more than once." << std::endl;
exit( 0 );
}
-
+
Node bd = TermDb::getFunDefBody( assertions[i] );
Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
if( !bd.isNull() ){
+ d_funcs.push_back( f );
bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
//create a sort S that represents the inputs of the function
//find finite models for well-defined functions
class FunDefFmf {
private:
- //defined functions to input sort
- std::map< Node, TypeNode > d_sorts;
- //defined functions to injections input -> argument elements
- std::map< Node, std::vector< Node > > d_input_arg_inj;
//simplify
Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def = 0 );
//simplify term
public:
FunDefFmf(){}
~FunDefFmf(){}
-
+ //defined functions to input sort (alpha)
+ std::map< Node, TypeNode > d_sorts;
+ //defined functions to injections input -> argument elements (gamma)
+ std::map< Node, std::vector< Node > > d_input_arg_inj;
+ // (newly) defined functions
+ std::vector< Node > d_funcs;
+ //simplify
void simplify( std::vector< Node >& assertions, bool doRewrite = false );
};
#include "theory/quantifiers/macros.h"
#include "theory/rewriter.h"
#include "proof/proof_manager.h"
+#include "smt/smt_engine_scope.h"
using namespace CVC4;
using namespace std;
retVal = true;
}
}
+ //also store as defined functions
+ for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
+ Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
+ Trace("macros-def") << " basis is : ";
+ std::vector< Node > nargs;
+ std::vector< Expr > args;
+ for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
+ Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
+ Trace("macros-def") << d_macro_basis[it->first][i] << " ";
+ nargs.push_back( bv );
+ args.push_back( bv.toExpr() );
+ }
+ Trace("macros-def") << std::endl;
+ Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
+ smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+ }
}
return retVal;
}
}
}
if( !coeff.isNull() ){
- term = NodeManager::currentNM()->mkNode( PLUS, plus_children );
+ term = plus_children.size()==1 ? plus_children[0] : NodeManager::currentNM()->mkNode( PLUS, plus_children );
term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );
}
}
incremental-subst-bug.cvc
SMT2_TESTS = \
- tiny_bug.smt2
+ tiny_bug.smt2
BUG_TESTS = \
bug216.smt2 \
bug233.cvc \
bug326.smt2 \
arith_lra_01.smt2 \
- arith_lra_02.smt2
+ arith_lra_02.smt2 \
+ quant-fun-proc.smt2 \
+ quant-fun-proc-unmacro.smt2 \
+ quant-fun-proc-unfd.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
--- /dev/null
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+(set-logic UFLIA)
+
+
+(define-fun f ((x Int)) Int x)
+
+(declare-fun h (Int) Int)
+(assert (forall ((x Int)) (= (h x) 0)))
+
+; EXPECT: sat
+(push 1)
+(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
+(check-sat)
+(pop 1)
+
+(declare-fun g (Int) Int)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (f 1) 2))
+(check-sat)
+(pop 1)
+
+; EXPECT: sat
+(push 1)
+(assert (= (g 1) 5))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (h 1) 5))
+(check-sat)
+(pop 1)
--- /dev/null
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+(set-logic UFLIA)
+
+
+(define-fun f ((x Int)) Int x)
+
+(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
+
+; EXPECT: sat
+(declare-fun h (Int) Int)
+(push 1)
+(assert (forall ((x Int)) (= (h x) 0)))
+(check-sat)
+(pop 1)
+
+
+; EXPECT: unsat
+(push 1)
+(assert (= (f 1) 2))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (g 1) 5))
+(check-sat)
+(pop 1)
+
+; EXPECT: sat
+(push 1)
+(assert (= (h 1) 5))
+(check-sat)
+(pop 1)
+
--- /dev/null
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+(set-logic UFLIA)
+
+(define-fun f ((x Int)) Int x)
+
+(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
+
+(declare-fun h (Int) Int)
+(assert (forall ((x Int)) (= (h x) (+ x 3))))
+
+; EXPECT: sat
+(check-sat)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (f 1) 2))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (g 1) 5))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (h 1) 5))
+(check-sat)
+(pop 1)
projects / cvc5.git / commitdiff