Variables created during propagator initialization are not frozen and might be eliminated by preprocessing.

[MaxOstrowski]

bug.zip

While calling
clingcon encoding.lp types.lp test.lp --stats 0
gives the expected results
adding any --conf=XXX like jumpy results in a segfault.

[MaxOstrowski]

Could bring it down to

{b;c}.                                                                                                 
&sum{a} = 2 :- b.                                                                                      
&sum{a} = 3 :- c.

calling with enumerating all models 0 and conf=jumpy

[rkaminsk]

I think that this is a bug in clasp. If I run this with valgrind, I get a bug while a conflict is analyzed. @BenKaufmann can you please have a look? The example is luckily tiny:

clingcon/build/debug on  wip […] took 6s ➜ valgrind --num-callers=100 ./bin/clingcon --conf=jumpy 0 test.lp
==35202== Memcheck, a memory error detector
==35202== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==35202== Using Valgrind-3.15.0 and LibVEX; rerun with -h for copyright info
==35202== Command: ./bin/clingcon --conf=jumpy 0 test.lp
==35202== 
clingcon version 5.0.0
Reading from test.lp
Solving...
clingcon: /home/kaminski/git/clingo/clasp/clasp/solver.h:773: void Clasp::Solver::markLevel(Clasp::uint32): Assertion `validLevel(dl)' failed.
==35202== 
==35202== Process terminating with default action of signal 6 (SIGABRT)
==35202==    at 0x56C918B: raise (raise.c:51)
==35202==    by 0x56A8858: abort (abort.c:79)
==35202==    by 0x56A8728: __assert_fail_base.cold (assert.c:92)
==35202==    by 0x56B9F35: __assert_fail (assert.c:101)
==35202==    by 0x4FD03AE: Clasp::Solver::markLevel(unsigned int) (solver.h:773)
==35202==    by 0x50500F3: Clasp::Solver::analyzeConflict() (solver.cpp:1195)
==35202==    by 0x504E340: Clasp::Solver::resolveConflict() (solver.cpp:917)
==35202==    by 0x5053DCC: Clasp::Solver::search(Clasp::SearchLimits&, double) (solver.cpp:1809)
==35202==    by 0x5045848: Clasp::BasicSolve::State::solve(Clasp::Solver&, Clasp::SolveParams const&, Clasp::SolveLimits*) (solve_algorithms.cpp:184)
==35202==    by 0x5044A93: Clasp::BasicSolve::solve() (solve_algorithms.cpp:81)
==35202==    by 0x5047A11: Clasp::SequentialSolve::doSolve(Clasp::SharedContext&, bk_lib::pod_vector<Clasp::Literal, std::allocator<Clasp::Literal> > const&) (solve_algorithms.cpp:452)
==35202==    by 0x5046A47: Clasp::SolveAlgorithm::solve(Clasp::SharedContext&, bk_lib::pod_vector<Clasp::Literal, std::allocator<Clasp::Literal> > const&, Clasp::ModelHandler*)::Scoped::solve(bk_lib::pod_vector<Clasp::Literal, std::allocator<Clasp::Literal> > const&) (solve_algorithms.cpp:326)
==35202==    by 0x5046ACA: Clasp::SolveAlgorithm::solve(Clasp::SharedContext&, bk_lib::pod_vector<Clasp::Literal, std::allocator<Clasp::Literal> > const&, Clasp::ModelHandler*) (solve_algorithms.cpp:330)
==35202==    by 0x4F7BCE9: Clasp::ClaspFacade::SolveStrategy::startAlgo(Clasp::SolveMode_t) (clasp_facade.cpp:323)
==35202==    by 0x4F82B58: Clasp::ClaspFacade::SolveStrategy::doStart() (clasp_facade.cpp:271)
==35202==    by 0x4F7BB70: Clasp::ClaspFacade::SolveStrategy::start(Clasp::EventHandler*, bk_lib::pod_vector<Clasp::Literal, std::allocator<Clasp::Literal> > const&) (clasp_facade.cpp:312)
==35202==    by 0x4F7FA4B: Clasp::ClaspFacade::solve(Clasp::SolveMode_t, bk_lib::pod_vector<Clasp::Literal, std::allocator<Clasp::Literal> > const&, Clasp::EventHandler*) (clasp_facade.cpp:991)
==35202==    by 0x4C381D7: Gringo::ClingoSolveFuture::ClingoSolveFuture(Gringo::ClingoControl&, Clasp::SolveMode_t) (clingocontrol.cc:761)
==35202==    by 0x4C40AAB: std::unique_ptr<Gringo::ClingoSolveFuture, std::default_delete<Gringo::ClingoSolveFuture> > Gringo::gringo_make_unique<Gringo::ClingoSolveFuture, Gringo::ClingoControl&, Clasp::SolveMode_t>(Gringo::ClingoControl&, Clasp::SolveMode_t&&) (utility.hh:404)
==35202==    by 0x4C354AD: Gringo::ClingoControl::solve(Potassco::Span<int>, unsigned int, std::unique_ptr<Gringo::SolveEventHandler, std::default_delete<Gringo::SolveEventHandler> >) (clingocontrol.cc:363)
==35202==    by 0x4C60457: clingo_control_solve (control.cc:1290)
==35202==    by 0x116C03: Clingo::Control::solve(Clingo::Span<int, Clingo::ToIterator<int> >, Clingo::SolveEventHandler*, bool, bool) (clingo.hh:4185)
==35202==    by 0x1167AD: Clingo::Control::solve(Clingo::Span<Clingo::SymbolicLiteral, Clingo::ToIterator<Clingo::SymbolicLiteral> >, Clingo::SolveEventHandler*, bool, bool) (clingo.hh:4142)
==35202==    by 0x117D39: ClingconApp::main(Clingo::Control&, Clingo::Span<char const*, Clingo::ToIterator<char const*> >) (main.cc:156)
==35202==    by 0x113F2F: Clingo::Detail::g_main(clingo_control*, char const* const*, unsigned long, void*) (clingo.hh:4572)
==35202==    by 0x4C6293B: (anonymous namespace)::CClingoApp::main(Gringo::ClingoControl&, std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&) (control.cc:1638)
==35202==    by 0x4C346E7: Gringo::ClingoControl::main(Gringo::IClingoApp&, std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, Gringo::ClingoOptions const&, Clasp::Asp::LogicProgram*) (clingocontrol.cc:246)
==35202==    by 0x4C21808: Gringo::ClingoApp::run(Clasp::ClaspFacade&) (clingo_app.cc:281)
==35202==    by 0x4C79912: Clasp::Cli::ClaspAppBase::run() (clasp_app.cpp:217)
==35202==    by 0x50BA658: Potassco::Application::main(int, char**) (application.cpp:127)
==35202==    by 0x4C6306F: clingo_main (control.cc:1697)
==35202==    by 0x116F44: Clingo::clingo_main(Clingo::Application&, Clingo::Span<char const*, Clingo::ToIterator<char const*> >) (clingo.hh:5393)
==35202==    by 0x1142D1: main (main.cc:182)
==35202== 
==35202== HEAP SUMMARY:
==35202==     in use at exit: 46,099 bytes in 647 blocks
==35202==   total heap usage: 2,252 allocs, 1,605 frees, 259,262 bytes allocated
==35202== 
==35202== LEAK SUMMARY:
==35202==    definitely lost: 32 bytes in 2 blocks
==35202==    indirectly lost: 0 bytes in 0 blocks
==35202==      possibly lost: 9,822 bytes in 174 blocks
==35202==    still reachable: 36,245 bytes in 471 blocks
==35202==                       of which reachable via heuristic:
==35202==                         newarray           : 1,584 bytes in 1 blocks
==35202==         suppressed: 0 bytes in 0 blocks
==35202== Rerun with --leak-check=full to see details of leaked memory
==35202== 
==35202== For lists of detected and suppressed errors, rerun with: -s
==35202== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
zsh: abort (core dumped)  valgrind --num-callers=100 ./bin/clingcon --conf=jumpy 0 test.lp

[rkaminsk]

For easy reproduction:

#!/usr/bin/bash

j=`grep processor /proc/cpuinfo | wc -l`

git clone https://github.com/potassco/clingo.git --recursive
git clone https://github.com/potassco/clingcon.git

cmake -Hclingo -Bbuild/clingo -DCMAKE_BUILD_TYPE=Debug -DPYCLINGO_USER_INSTALL=Off -DPYCLINGO_USE_INSTALL_PREFIX=On -DCMAKE_INSTALL_PREFIX=install
cmake --build build/clingo --target install -j${j}

cmake -Hclingcon -Bbuild/clingcon -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=install
cmake --build build/clingcon --target install -j${j}

./install/bin/clingcon --conf=jumpy 0 <<EOF
{b;c}.
&sum{a} = 2 :- b.
&sum{a} = 3 :- c.
EOF

[BenKaufmann]

Interesting. Seems to be related to sat-preprocessing.

./install/bin/clingcon --conf=jumpy --no-sat-pre 0 <<EOF
{b;c}.
&sum{a} = 2 :- b.
&sum{a} = 3 :- c.
EOF

works fine, while

./install/bin/clingcon --sat-pre 0 <<EOF
{b;c}.
&sum{a} = 2 :- b.
&sum{a} = 3 :- c.
EOF

also results in an assertion.

[BenKaufmann]

This is not really a bug in clasp but more a manifestation of undefined behaviour due to a precondition violation. clingcon adds new variables that are relevant in "theory constraints" but does not explicitly mark these as frozen. clasp's sat-preprocessor otoh assumes that all variables that are not explicitly marked as frozen only occur in the set of currently known clauses and can therefore be eliminated by clause distribution (among other things). Once a variable has been eliminated, it is assumed that it is no longer part of any (explicit or implicit) constraint.
In this particular case a newly introduced variable is eliminated by the sat-preprocessor but then later assigned by some clingcon-constraint. This is not allowed and eventually results in the assertion failure.

One easy fix for this problem would be to change clingo's ClingoPropagateInit::addLiteral() to something like this:

Potassco::Lit_t addLiteral() override {
  auto v = facade_().ctx.addVar(Clasp::Var_t::Atom);
  facade_().ctx.setFrozen(v, true);
  return Clasp::encodeLit(Clasp::posLit(v));
}

Alternatively, one could come up with a more fine-grained approach, e.g. by freezing only those variables for which addWatch() is called or by introducing an explicit API.

[rkaminsk]

I guess that from a clingcon perspective, we would have to freeze all variables anyway except if we translate all constraints to clauses during propagate init. What do you think about adding a flag to addLiteral() to request a frozen/static variable?

And one more general question. Do you think it is necessary in general that a propagator freezes variables it wants to add constraints over?

[BenKaufmann]

I guess that from a clingcon perspective, we would have to freeze all variables anyway except if we translate all constraints to clauses during propagate init. What do you think about adding a flag to addLiteral() to request a frozen/static variable?

I think an explicit flag is definitely better than some implicit heuristic. But I would only add it if you think that "eagerly translating all constraints up front" is a relevant use-case. Otherwise, I would probably just unconditionally freeze all variables added via PropagateInit.

And one more general question. Do you think it is necessary in general that a propagator freezes variables it wants to add constraints over?

Yes. However, you only have to freeze variables that are added during initialization (PropagateInit). Solver-local variables added via PropagateControl are not subject to sat-preprocessing.

[rkaminsk]

I guess that from a clingcon perspective, we would have to freeze all variables anyway except if we translate all constraints to clauses during propagate init. What do you think about adding a flag to addLiteral() to request a frozen/static variable?

I think an explicit flag is definitely better than some implicit heuristic. But I would only add it if you think that "eagerly translating all constraints up front" is a relevant use-case. Otherwise, I would probably just unconditionally freeze all variables added via PropagateInit.

In clingcon we have the use case. There are some variables that a solver has to watch and some that are just auxiliary variables that could be resolved away.

And one more general question. Do you think it is necessary in general that a propagator freezes variables it wants to add constraints over?

Yes. However, you only have to freeze variables that are added during initialization (PropagateInit). Solver-local variables added via PropagateControl are not subject to sat-preprocessing.

We also have propagators that do not add any variables at all but just use variables associated with atoms. I wanted to ask if those variables have to be frozen as well if the propagator wants to add clauses over them?

[BenKaufmann]

We also have propagators that do not add any variables at all but just use variables associated with atoms. I wanted to ask if those variables have to be frozen as well if the propagator wants to add clauses over them?

Yes. But clasp already marks all variables associated with input atoms as frozen if program updates are enabled via ClaspFacade::enableProgramUpdates().

[rkaminsk]

I see. In clingo this is atm always enabled. But I was thinking to provide a way to disable program updates because a lot of users were asking for a mode where the library would behave exactly as clasp's single shot solving. What do you think about the following? We freeze variables added during propagator initialization if program updates are enabled and otherwise don't. In the API, I can add a function to freeze variables and to disable program updates. This gives experts the possibility to tune single-shot solving even with propagators and there are fewer pitfalls in the standard case.

[BenKaufmann]

Sounds reasonable to me.

[rkaminsk]

Sounds reasonable to me.

I think I don't even need your help to implement this. This can all be done in clingo. At least I hope so. I'll let you know if I need anything. Thanks for having a look.

[MaxOstrowski]

Thanks guys, this sounds awesome.
Will it be possible to introduce unfreezed variables in the multi shot case (with Program updates enabled) ?

[rkaminsk]

I was thinking to provide a way to disable program updates because a lot of users were asking for a mode where the library would behave exactly as clasp's single shot solving.

I cannot provide an option to disable program updates because the clingo API needs access to program literals from the logic program in the model callback (and there is no (reasonable) way around this). I will simply provide PropagateInit::freeze and PropagateInit::unfreeze methods and add a default enabled freeze flag to the PropagateInit::add_literal method. The (expert) user (who read the source code) knows best what to freeze/unfreeze anyway.

EDIT: Providing an unfreeze method is probably a bad idea because it will be hard to use correctly. Having a freeze method in the single-shot case is probably useful though. See my comment below for another idea.

[rkaminsk]

@BenKaufmann I had a look at clasp's facade. Currently ClaspFacade::prepare releases the the logic program whenever program updates have not been enabled. I think that all I need to enable single shot solving with the API is to prevent the facade from deleting the logic program. Would it be (easily) possible to add an option for this? Maybe just a function to initialize ClaspFacade::accu_? Would it still be possible to get the truth value of (selected) atoms in the logic program in the model callback even if their associated variables were eliminated? Or does clasp freeze all "output" atoms anyway?

EDIT: If none of this is viable, I would simply not provide single-shot solving and leave it at 1a8512c.

[BenKaufmann]

I think that all I need to enable single shot solving with the API is to prevent the facade from deleting the logic program.
Would it be (easily) possible to add an option for this? Maybe just a function to initialize ClaspFacade::accu_?

Initializing ClaspFacade::accu_ wouldn't help. It is only needed/useful in the context of multi-step solving. Instead, we would have to change LogicProgram::dispose() so that it does not automatically remove the whole program if program updates are not enabled, ClaspFacade should then distinguish three modes: a) single-shot, no-script, b) singleshot, with script, c) multishot and call
LogicProgram::dispose(true) only if mode a) is active.

Would it still be possible to get the truth value of (selected) atoms in the logic program in the model callback even if their
associated variables were eliminated? Or does clasp freeze all "output" atoms anyway?

Clasp does not freeze "output" atoms and eliminated variables are not part of a solver assignment. However, models are always extended to all variables and hence also contain an assignment for eliminated variables.

[rkaminsk]

Initializing ClaspFacade::accu_ wouldn't help. It is only needed/useful in the context of multi-step solving. Instead, we would have to change LogicProgram::dispose() so that it does not automatically remove the whole program if program updates are not enabled, ClaspFacade should then distinguish three modes: a) single-shot, no-script, b) singleshot, with script, c) multishot and call LogicProgram::dispose(true) only if mode a) is active.

I thought that initializing acc_ without setting incremental mode would give us something like mode b) because the program won't be disposed. We might even need it to keep so that the on_statistics callback I implemented stays special-case free.

Clasp does not freeze "output" atoms and eliminated variables are not part of a solver assignment. However, models are always extended to all variables and hence also contain an assignment for eliminated variables.

This would mean that in mode b) I would also have to adjust the cleanup function because I can no longer assume that a program literal is associated with a valid solver literal. It looks like this feature would require quite a lot of testing on my side. Maybe better skip it.

void ClingoControl::cleanup() {
    if (!clingoMode_ || !canClean_) {
        return;
    }
    canClean_ = false;
    Clasp::Asp::LogicProgram &prg = static_cast<Clasp::Asp::LogicProgram&>(*clasp_->program());
    Clasp::Solver &solver = *clasp_->ctx.master();
    auto assignment = [&prg, &solver](unsigned uid) {
        Potassco::Value_t truth{Potassco::Value_t::Free};
        bool external{false};
        if (prg.validAtom(uid)) {
            external = prg.isExternal(uid);
            Clasp::Literal lit = prg.getLiteral(uid);
            if (solver.isTrue(lit)) { truth = Potassco::Value_t::True; }
            else if (solver.isFalse(lit)) { truth = Potassco::Value_t::False; }
        }
        return std::make_pair(external, truth);
    };
    auto stats = out_->simplify(assignment);
    LOG << stats.first << " atom" << (stats.first == 1 ? "" : "s") << " became facts" << std::endl;
    LOG << stats.second << " atom" << (stats.second == 1 ? "" : "s") << " deleted" << std::endl;
}

[rkaminsk]

I am keeping it simple. Closing this.