Wrong get-value response using IDL

[Marc Massot]

Hi,

We are using OpenSMT using this input:

(set-logic QF_IDL)
(set-info :smt-lib-version 2.0)
(declare-fun s_0 () Int)
(declare-fun s_1 () Int)
(assert (and
(or (= s_0 0) (= s_0 1) (= s_0 2))
(or (= s_1 0) (= s_1 1) (= s_1 2))
(> s_1 s_0)
))
(check-sat)
(get-value (s_0 s_1))
(exit)

But it prints a wrong reponse:

s_0: 4
s_1: 5

Could someone give us an explanation for this behavior?

We are using our implementation of GetValue, because get-value is not
implemented yet:

void OpenSMTContext::GetValue ( Enode * e) {
if ( state == l_True) {
ostream & out = config.getRegularOut( );
Enode * aux = e;
while (!aux->isEnil()) {
Enode * atom = aux->getCar();
if (atom->isAtom()) {
lbool value = getModel(atom);
if ( value == l_True )
{
out << atom << ": true" <<
endl;
}
else if ( value == l_False )
{
out << atom << ": false" <<
endl;
}
else {
out << atom << ": undef" <<
endl;
}
}
else if (atom->isVar()) {
if (atom->hasValue()) {
out << atom << ": " << atom-
>getValue() << endl;
}
else {
out << atom << ": var without
value" << endl;
}
}
else {
out << "I couldn't retrieve the value
of " << atom << endl;
}
aux = aux->getCdr();
}
}
else {
opensmt_warning ("Skipping command (get-value) as
formula is not sat");
}
}

Thanks!!

[Luis Renato Santos]

Hi,

I need to use the OpenSMT with the get-value command, can you explain me how i can use your implementation?

[lu.d...@gmail.com]

 

OpenSMT didnt offer "getvalue" command directly as far as I know,you should  modify the code if you want to get the value.

 

ldsir_gmail，lu.d...@gmail.com

2012/12/4

--
You received this message because you are subscribed to the Google Groups "opensmt" group.
To view this discussion on the web visit https://groups.google.com/d/msg/opensmt/-/yG00d4rT7AUJ.
To post to this group, send email to ope...@googlegroups.com.
To unsubscribe from this group, send email to opensmt+u...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/opensmt?hl=en.

[Joan Espasa]

This code should go into: src/api/OpenSMTContext.C and src/api/OpenSMTContext.h

Also, you should add to the command to the parsing structure.

[Luis Renato Santos]

Thanks by the informations. But, I don't know how to add the command to the parsing structure. Can you help me again?

[Luis Renato Santos]

Can anyone help me to use the command get-value? I tryed paste this code in src/api/OpenSMTContext.C and add a command in src/api/OpenSMTContext.h, but when i compile the code, shows a message error.