From: ajreynol Date: Thu, 26 Nov 2015 13:08:33 +0000 (+0100) Subject: Front-end support for get-value of sort cardinality, minor fixes for sygus solution... X-Git-Tag: cvc5-1.0.0~6159 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=365d6022b5742fc6910363e04e873b26e221bb05;p=cvc5.git Front-end support for get-value of sort cardinality, minor fixes for sygus solution reconstruction. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8dce0b639..d2409ba15 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2214,6 +2214,7 @@ builtinOp[CVC4::Kind& kind] | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } + | FMFCARDVAL_TOK { $kind = CVC4::kind::CARDINALITY_VALUE; } | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } // NOTE: Theory operators no longer go here, add to smt2.cpp. Only @@ -2613,6 +2614,7 @@ REALLCHAR_TOK : 're.allchar'; DTSIZE_TOK : 'dt.size'; FMFCARD_TOK : 'fmf.card'; +FMFCARDVAL_TOK : 'fmf.card.val'; INST_CLOSURE_TOK : 'inst-closure'; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b9b309d4a..56ad9c35a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -446,6 +446,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::REGEXP_EMPTY: out << "re.nostr "; break; case kind::REGEXP_SIGMA: out << "re.allchar "; break; + case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; + case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; + // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; forceBinary = true; break; case kind::BITVECTOR_AND: out << "bvand "; forceBinary = true; break; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 914c0614f..822baaaaf 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -865,32 +865,42 @@ struct sortSiInstanceIndices { } }; -/* -Node removeBooleanIte( Node n ){ + +Node CegConjectureSingleInv::postProcessSolution( Node n ){ + /* + ////remove boolean ITE (not allowed for sygus comp 2015) if( n.getKind()==ITE && n.getType().isBoolean() ){ - Node n1 = removeBooleanIte( n[1] ); - Node n2 = removeBooleanIte( n[2] ); + Node n1 = postProcessSolution( n[1] ); + Node n2 = postProcessSolution( n[2] ); return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ), NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) ); }else{ - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; imkNode( n.getKind(), children ); - }else{ - return n; + */ + bool childChanged = false; + Kind k = n.getKind(); + if( n.getKind()==INTS_DIVISION_TOTAL ){ + k = INTS_DIVISION; + childChanged = true; + }else if( n.getKind()==INTS_MODULUS_TOTAL ){ + k = INTS_MODULUS; + childChanged = true; + } + std::vector< Node > children; + for( unsigned i=0; imkNode( k, children ); + }else{ + return n; } } -*/ + Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){ Assert( d_sol!=NULL ); @@ -994,9 +1004,12 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl; } }else{ - ////remove boolean ITE (not allowed for sygus comp 2015) - //d_solution = removeBooleanIte( d_solution ); - //Trace("csi-sol") << "Solution (after remove boolean ITE) : " << d_solution << std::endl; + Trace("csi-sol") << "Post-process solution..." << std::endl; + Node prev = d_solution; + d_solution = postProcessSolution( d_solution ); + if( prev!=d_solution ){ + Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl; + } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 0bdf246f0..99dcaabb9 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -72,6 +72,7 @@ private: void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); //constructing solution Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ); + Node postProcessSolution( Node n ); private: //map from programs to variables in single invocation property std::map< Node, Node > d_single_inv_map; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index c62a0dd4a..44e4193eb 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -88,11 +88,14 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ //for now, we only handle cardinalities for uninterpreted sorts if( tn.isSort() ){ if( d_rep_set.hasType( tn ) ){ + Debug("model-getvalue-debug") << "Get cardinality sort, #rep : " << d_rep_set.getNumRepresentatives( tn ) << std::endl; return Cardinality( d_rep_set.getNumRepresentatives( tn ) ); }else{ - return Cardinality( CardinalityUnknown() ); + Debug("model-getvalue-debug") << "Get cardinality sort, unconstrained, return 1." << std::endl; + return Cardinality( 1 ); } }else{ + Debug("model-getvalue-debug") << "Get cardinality other sort, unknown." << std::endl; return Cardinality( CardinalityUnknown() ); } } @@ -191,7 +194,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const ret = Rewriter::rewrite(ret); Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl; if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) { + Debug("model-getvalue-debug") << "get cardinality constraint " << ret[0].getType() << std::endl; ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst().getNumerator()); + }else if(ret.getKind() == kind::CARDINALITY_VALUE) { + Debug("model-getvalue-debug") << "get cardinality value " << ret[0].getType() << std::endl; + ret = NodeManager::currentNM()->mkConst(Rational(getCardinality(ret[0].getType().toType()).getFiniteCardinality())); } d_modelCache[n] = ret; return ret; diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index ccdac32ab..f0b50b778 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -21,4 +21,7 @@ typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRul operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature" typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule +operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S" +typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule + endtheory diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 93fd1dc6f..0040a38c3 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -99,6 +99,17 @@ public: } };/* class CardinalityConstraintTypeRule */ +class CardinalityValueTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + if( check ) { + n[0].getType(check); + } + return nodeManager->integerType(); + } +};/* class CardinalityValueTypeRule */ + }/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */