From 0615601703a1ac19d485e2b530a748c797b544ed Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 1 Feb 2016 11:18:00 -0600 Subject: [PATCH] Simplify fmc model construction, add regression. Improve FMF debug assertions. --- src/theory/quantifiers/first_order_model.cpp | 3 ++ src/theory/quantifiers/term_database.cpp | 29 ++++++++++++++++---- src/theory/quantifiers/term_database.h | 3 ++ test/regress/regress0/fmf/Makefile.am | 3 +- test/regress/regress0/fmf/am-bad-model.cvc | 22 +++++++++++++++ 5 files changed, 54 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress0/fmf/am-bad-model.cvc diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 018a0c3e0..aa2a43fbf 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -669,6 +669,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { Node v = d_models[op]->d_value[i]; Trace("fmc-model-func") << "Value is : " << v << std::endl; + Assert( v.isConst() ); + /* if( !hasTerm( v ) ){ //can happen when the model basis term does not exist in ground assignment TypeNode tn = v.getType(); @@ -685,6 +687,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { } } v = getRepresentative( v ); + */ if( curr.isNull() ){ Trace("fmc-model-func") << "base : " << v << std::endl; curr = v; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 56f966426..6dfd4c737 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1605,10 +1605,10 @@ bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) { } bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) { - if( std::find( t.begin(), t.end(), n )!=t.end() ){ - return true; - }else{ - if( visited.find( n )==visited.end() ){ + if( visited.find( n )==visited.end() ){ + if( std::find( t.begin(), t.end(), n )!=t.end() ){ + return true; + }else{ visited[n] = true; for( unsigned i=0; i& t, std::map< Node, boo } } } - return false; } + return false; +} + +bool TermDb::containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ) { + if( n.getKind()==UNINTERPRETED_CONSTANT ){ + return true; + }else if( visited.find( n )==visited.end() ){ + visited[n] = true; + for( unsigned i=0; i& t ) { } } +bool TermDb::containsUninterpretedConstant( Node n ) { + std::map< Node, bool > visited; + return containsUninterpretedConstant2( n, visited ); +} + Node TermDb::simpleNegate( Node n ){ if( n.getKind()==OR || n.getKind()==AND ){ std::vector< Node > children; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 86b0efbf3..0c4e94517 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -397,12 +397,15 @@ private: //helper for contains term static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited ); static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); + static bool containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ); //general utilities public: /** simple check for whether n contains t as subterm */ static bool containsTerm( Node n, Node t ); /** simple check for contains term, true if contains at least one term in t */ static bool containsTerms( Node n, std::vector< Node >& t ); + /** contains uninterpreted constant */ + static bool containsUninterpretedConstant( Node n ); /** simple negate */ static Node simpleNegate( Node n ); /** is assoc */ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 8b7202906..370096a1e 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -48,7 +48,8 @@ TESTS = \ tail_rec.smt2 \ jasmin-cdt-crash.smt2 \ loopy_coda.smt2 \ - fmc_unsound_model.smt2 + fmc_unsound_model.smt2 \ + am-bad-model.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/am-bad-model.cvc b/test/regress/regress0/fmf/am-bad-model.cvc new file mode 100644 index 000000000..e30b5e04a --- /dev/null +++ b/test/regress/regress0/fmf/am-bad-model.cvc @@ -0,0 +1,22 @@ +% EXPECT: sat +OPTION "produce-models"; +OPTION "finite-model-find"; + +f : (BITVECTOR(2),BITVECTOR(2)) ->ARRAY INT OF INT; +f0 : BITVECTOR(2) -> ARRAY INT OF INT; + +td,td1,td2: ARRAY INT OF INT; +ASSERT td1 = td WITH[0]:= 1; +ASSERT td2 = td WITH[0]:= 2; +ASSERT f(0bin01,0bin00)=td1; +ASSERT f(0bin10,0bin00)=td2; +%ASSERT FORALL(i:BITVECTOR(2)) : f0(i)=f(0bin00,i) ; +%Artificial bypass of quantifier for f0 definition +ASSERT f0(0bin00) = f(0bin00,0bin00); +ASSERT f0(0bin01) = f(0bin00,0bin01); +ASSERT f0(0bin10) = f(0bin00,0bin10); +ASSERT f0(0bin11) = f(0bin00,0bin11); +ASSERT FORALL(i:BITVECTOR(2)) : f0(i)=td2 ; + +CHECKSAT; + -- 2.30.2