9 s <<
"(cRR _ _ _ _ @a" <<
abs(
d_var );
16 s <<
"(" << (
d_var>0 ?
"R" :
"Q" ) <<
" _ _ ";
25 s <<
"(res " <<
d_var;
42 std::vector< int > c[2];
43 for(
int a=0; a<2; a++ ){
46 for(
int b=0; b<(int)c[a].size(); b++ ){
48 c[a].erase( c[a].begin() + b, c[a].begin() + b + 1 );
57 for(
int b=0; b<(int)c[a].size(); b++ ){
58 if( std::find( clause.begin(), clause.end(), c[a][b] )==clause.end() ){
59 clause.push_back( c[a][b] );
67 const Expr& pf,
bool cascadeOr )
81 ose <<
"Error: Resolving on double negation" << cres;
90 return Make( p1, p2, m,
false );
95 ostringstream os1, os2;
97 os1 <<
"(c" << (m>0 ?
"R" :
"Q" );
98 os1 <<
" _ _ _ _ @a" <<
abs( m );
102 ostringstream os1, os2;
104 os1 <<
"(c" << (m>0 ?
"R" :
"Q" );
105 os1 <<
"0 _ _ _ @a" <<
abs( m );
115 s <<
"(clausify_form" << (
d_var<0 ?
"_not" :
"") <<
" _ _ @a" <<
abs(
d_var ) <<
" ";
124 std::vector< Expr > exprs;
138 exprs.push_back( e[0] );
143 for(
int a=0; a<(int)exprs.size(); a++ ){
144 ostringstream os1, os2;
145 os1 <<
"(or_elim_1 _ _ ";
146 int m =
queryM( exprs[a] );
148 os1 << ( m<0 ?
"(not_not_intro _ " :
"" );
149 os1 <<
"@v" <<
abs( m );
150 os1 << ( m<0 ?
")" :
"" );
164 s <<
"(as" << (m>0 ?
"t" :
"f") <<
" _ _ _ @a" <<
abs( m );
166 s <<
"(th_as" << (m>0 ?
"t" :
"f") <<
" _ ";
167 s <<
" (\\ @v" <<
abs( m ) <<
" ";
void print_struct(std::ostream &s, int ind=0)
void print_structure(std::ostream &s, int ind=0)
Data structure of expressions in CVC3.
static Expr cascade_expr(const Expr &e)
LFSCBoolRes(LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
int checkBoolRes(std::vector< int > &clause)
void print_pf(std::ostream &s, int ind=0)
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
static void print_error(const char *c, std::ostream &s)
static LFSCProof * Make(vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
static LFSCProof * Make_i(const Expr &e, LFSCProof *p, std::vector< Expr > &exprs, const Expr &end)
void print_pf(std::ostream &s, int ind=0)
virtual int checkBoolRes(std::vector< int > &clause)
void print_struct(std::ostream &s, int ind=0)
static LFSCProof * Make(int v, LFSCProof *pf)
RefPtr< LFSCProof > d_children[2]
void print_pf(std::ostream &s, int ind=0)
void print(std::ostream &s, int ind=0)
static LFSCProof * Make(int v, LFSCProof *pf, bool assm=true, int type=3)
static LFSCProof * MakeC(LFSCProof *p, const Expr &res)